perm filename GIVEN[AM,DBL] blob
sn#177113 filedate 1975-09-12 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00160 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00018 00002 .DEVICE XGP
C00019 00003 .PORTION TITLEPAGE
C00020 00004 .EVERY FOOTING(7{DATE}, Knowledge for Math Theory Formation, page GIVEN . {PAGE})
C00021 00005 3↓_SECTION 1: OVERVIEW OF BEINGS' FAMILIES_↓*
C00023 00006 5↓_ARCHETYPICAL BEINGS: BEINGS WHOSE NAMES ARE PART NAMES_↓*
C00027 00007 5Parts of each archetypical BEING* (one whose name is the name of a BEING part)
C00028 00008 5 ↓_OBJECT BEINGS: STATIC HOLDERS OF INFORMATION_↓
C00029 00009 5 Parts of Object BEINGs *
C00031 00010 5↓_ACTIVE BEINGS: DYNAMIC PROPERTIES AND RELATIONS_↓*
C00033 00011 5Parts of Relation BEINGs*
C00034 00012 5↓_STATIC META BEINGS: OBJECTS WITH JUSTIFICATIONS_↓*
C00035 00013 5Parts of Static Meta BEINGs*
C00036 00014 5↓_ACTIVE META BEINGS: ACTIONS WHICH AFFECT BEINGS_↓*
C00038 00015 5Parts of Active Meta BEINGs*
C00039 00016 5↓_ENVIRONMENTAL BEINGS: MODELS OF SYSTEM FUNCTIONS_↓*
C00041 00017 5↓_Awkward Beings: Those which don't fit in_↓*
C00043 00018 3↓_SECTION 2: THE ACTUAL INFO._↓* for each part of each BEING
C00044 00019 3ANY BEING* Knowledge which is not environmental, yet is common to all.
C00047 00020 3ARCHETYPE* BEINGs whose names are also part names. Strategies for part completion.
C00049 00021 2RECOGNITION GROUPING*
C00051 00022 2CHANGES* Is this rele. to producing the desired change in the world?
C00053 00023 2FINAL* What situations is this β rele. to bringing about?
C00055 00024 2PAST* Where is this used frequently, to advantage?
C00058 00025 2IDEN* {not}{quick} {fast} tests to see if this β is {not} currently referred to
C00060 00026 2ALTER GROUPING*
C00062 00027 2GENERALIZATIONS* What is this a special case of? How to make this more general.
C00065 00028 2SPECIALIZATIONS* Special cases of this? What new properties exist only there?
C00068 00029 2BOUNDARY* What marks the limits of this concept? Why exactly there?
C00072 00030 2DOMAIN/RANGE* Set of (what one can apply it to, what kind of thing one gets)
C00076 00031 2ORDERING*(Complete) What order should the parts be concentrated on (default)
C00079 00032 2WORTH* A vector of statistics which are monitored for user, environment, other β.
C00082 00033 2INTEREST* What special factors make β's interesting?
C00085 00034 2JUSTIFICATION* Why should one believe this? Formal/intu reasons. Efforts.
C00087 00035 2OPERATIONS* Associated with β. What can one do to it, what happens then?
C00090 00036 2ACT GROUPING*
C00092 00037 2CHANGE subgrouping of parts*
C00093 00038 2BOUNDARY-OPERATIONS*{not} Ops which patch {mews}up not-bdy-entities {bdy-entities}
C00095 00039 2FILLIN* How to initially fill it in, when and how to augment what is there already.
C00097 00040 2STRUCTURE* Whether, When, How to retructure (or split) this part.
C00099 00041 2ALGORITHMS* How to compute (for a relation, some 4doable* entity).
C00102 00042 2INTERPRET* subgrouping of parts
C00103 00043 2CHECK* How to examine and test out what is already there.
C00105 00044 2REPRESENTATION* How should entities of this type be represented internally?
C00108 00045 2VIEWS* How to view any β as a type of α. (e.g., a relation viewed as an object)
C00110 00046 2INFO GROUPING*
C00111 00047 2DEFINITION* Several alternative formal definitions of this concept.
C00114 00048 2INTU* Analogic interp., ties to simpler objects, to reality. Opaque.
C00117 00049 2TIES* Alterns. Parents/offspring. Analogies. Associated thms, conjecs, axioms, specific β's.
C00120 00050 2EXAMPLES* {not} {bdy} Includes trivial, typical, and advanced cases of each type.
C00125 00051 2CONTENTS* What is the value stored here, the actual contents of this entity.
C00127 00052 3OBJECT* Static holders of information.
C00129 00053 2ORDERED PAIR*
C00135 00054 2VARIABLE*
C00140 00055 2PROPOSITIONAL CONSTANT* Basic concept of simple true and false values.
C00143 00056 2STRUCTURE*
C00147 00057 2HIST*
C00150 00058 2LIST*
C00158 00059 2OSET* An ordered set a list with no repetitions of elements.
C00164 00060 2BAG*
C00171 00061 2SET*
C00180 00062 2ASSERTION*
C00182 00063 2AXIOM*
C00183 00064 3ACTIVE* Active Knowledge BEINGs operations, relations, and properites.
C00191 00065 2OPERATION* A way to transform members from one concept into another.
C00199 00066 2COMPOSITION* Apply an operation to the result of a previous operation.
C00206 00067 2INSERTION* Add new elements to a structure.
C00210 00068 2DELETION* Removal of an element from a structure.
C00214 00069 2CONVERT-STRUC* View the type x structure as a type y structure.
C00217 00070 2SUBSTITUTE* Replace one occurrence of x by y in S.
C00224 00071 2ASSIGN*
C00227 00072 2MAPSTRUC* Replace each member of a structure by the result of applying an Active to it.
C00232 00073 2REVERSE ORDERED PAIR*
C00236 00074 2RULE OF INFERENCE* Combine true statements into new, true ones.
C00243 00075 2DISJUNCTION*
C00247 00076 2CONJUNCTION*
C00251 00077 2NEGATION* This is a crucial process, which must be very knowledgable.
C00255 00078 2IMPLICATION*
C00261 00079 2UNITE* Join two structures together.
C00265 00080 2UNION* Join two sets together.
C00268 00081 2CROSS-PRODUCT* Join two sets together into a set of ordered pairs.
C00273 00082 2COMMON-PARTS* Find each x which is substruc. of 2 given strucs.
C00277 00083 2INTERSECTION* Find the common part of two given sets.
C00280 00084 2SETDIFFERENCE*
C00284 00085 2PUT-IN-ORDER* Arrange elements into some desired sequence.
C00289 00086 2RELATION* A conection between an ordered pair of BEINGs.
C00295 00087 @2SPECIFIC RELATIONS*
C00296 00088 2EQUALITY*
C00300 00089 2MEMBERSHIP* What structure(s) does a certain object belong to?
C00304 00090 2CONTAINMENT* What int/existing struct(s) is the given one a substruc of?
C00311 00091 2EQUIVALENCE*
C00324 00092 2SCOPE* Binding variables analysis of bound vs. free.
C00329 00093 2QUANTIFICATION*
C00333 00094 2UNIVERSAL QUANTIFICATION* For all "var" in "set", "statement" holds.
C00336 00095 2EXISTENTIAL QUANTIFICATION* There exists...
C00339 00096 2UNIVERSALLY NEGATIVE QUANTIFICATION* Never... For no...
C00341 00097 2EXISTENTIALLY NEGATIVE QUANTIFICATION* Not for all... For some x, not...
C00343 00098 2NEITHER NEVER NOR ALWAYS* For some, but not for all...
C00345 00099 2PROPERTY* A predicate, a condition which an entity might satisfy or not.
C00351 00100 2ORDERED* Are a structure's elements in proper precedence sequence?
C00358 00101 2CLOSURE* Generate a substructure from a core, using an operation.
C00366 00102 2EXTREME* Within a given example of a β, what are the subconcepts specifying its extremities.
C00374 00103 2ACTIVE.OPERATIONS* Properties, e.g. inverse, compose, repeat, function,...
C00378 00104 3STATIC META BEINGs* Higher-level constructions.
C00385 00105 2STATEMENT* An expression of some thought.
C00389 00106 2CONJECTURE*
C00393 00107 2STATEMENT OF GENERALITY*
C00397 00108 2STATEMENT OF EXISTENCE*
C00401 00109 2THEOREM*
C00407 00110 2PROOF*
C00414 00111 2COUNTEREXAMPLE*
C00419 00112 2CONTRADICTION* Notice that this might be tied into the environment (belief)
C00424 00113 2BUG* The only other type of known error, except for Contradiction.
C00428 00114 2ANALOGY*
C00434 00115 2MESSAGE* A structured communication (BEING↔BEING or user↔BEING)
C00438 00116 2ASSUMPTION*
C00442 00117 2MATHEMATICAL THEORY*
C00448 00118 2FOUNDATION*
C00452 00119 2BASIS*
C00455 00120 2FORMAL SYSTEM*
C00456 00121 3ACTIVE META BEINGs* Actions which affect BEINGS
C00459 00122 2FIND* Search for a member of a space satisfying some desired criteria.
C00466 00123 2SELECT* Choose one thing from among an explicit collection.
C00473 00124 2GUESS* Creatively produce a new conjecture, perhaps answering a given query
C00478 00125 2ELLIPSIS* And so on ... extrapolate infer from examples.
C00485 00126 2ANALOGIZE* Creatively produce a new analogy.
C00492 00127 2CONSERVATION* Inertia frame problem invariance compressability.
C00497 00128 2EXAMINE* prior to attemping pf. or disproof which is more likely?
C00498 00129 2TEST* Settle a claim. Prove or disprove a conjecture.
C00502 00130 2ASSUME*
C00504 00131 2DEFINE* Actually, this is an elaboration of DEFINITION.FILLIN.
C00508 00132 2PROVE* Formally establish a statement as a valid true fact.
C00514 00133 2LOGICALLY DEDUCE* Natural deduction.
C00519 00134 2PROVE DIRECTLY*
C00524 00135 2CASES* Wealky partition the possible situations and prove separately for each class.
C00533 00136 2BACKWARD CHAINING* Produce a direct proof, but by working backward from the goal.
C00537 00137 2PROVE INDIRECTLY* Assume the conjec. is false, and derive a contradiction.
C00541 00138 2PROVE ∀'s* Establishing universal conjectures, statements of generality.
C00547 00139 2MATHEMATICALLY INDUCE*
C00554 00140 2PROVE EXISTENCE* Establishing existential conjectures, statements of existence.
C00559 00141 2CONSTRUCTIVELY PROVE EXISTENCE* Build up an example to prove one exists.
C00565 00142 2NONCONSTRUCTIVELY DEDUCE EXISTENCE* Prove that some such entity, though unknown, 4must* exist.
C00570 00143 2DISPROVE* Establish definitively that conjecture x is false, invalid.
C00574 00144 2CONSTRUCTIVELY DISPROVE* Directly establish the falsity.
C00575 00145 2INDIRECTLY DISPROVE* Generally nonconstructive.
C00576 00146 2DEBUG* Correct, eliminate a bug.
C00580 00147 2COMMUNICATE* Create, translate, and analyze messages.
C00583 00148 2COMMUNIC. with USER"¬
C00584 00149 2TRANSLATE English into Beings*
C00585 00150 2TRANSLATE Beings into English*
C00586 00151 2USER* Model of the human user.
C00587 00152 2COMMUNIC. with other BEINGs*
C00588 00153 2RELATION META BEINGs* Active meta-Beings which are relations more than operations.
C00591 00154 2ISOMORPHISM* Equivalence of a pair of mathematical theories .
C00594 00155 2CATEGORICITY* Uniqueness of any set of axioms for a math theory with a given basis.
C00598 00156 3ENVIRONMENT* Model of system functions.
C00599 00157 2BELIEF*
C00600 00158 2INTERESTINGNESS* 7Notice this differs from the archetypical part-name Interest.*
C00601 00159 2CONTROL*
C00602 00160 .PORTION CONTENTS
C00603 ENDMK
C⊗;
.DEVICE XGP
.!XGPCOMMANDS←"/TMAR=40/PMAR=2120/BMAR=40"
.FONT 1 "BDR25"
.FONT 2 "BDR40"
.FONT 4 "BDI25"
.FONT 5 "BASB30"
.FONT 7 "NGR20"
.TURN ON "↑↓_π{"
.TURN ON "⊗" FOR "%"
.TURN ON "@" FOR "%"
.PAGE FRAME 66 HIGH 89 WIDE
.AREA TEXT LINES 3 TO 64
.AREA HEADING LINES 1 TO 2
.AREA FOOTING LINE 66
.!XGPLFTMAR←200
.NOFILL
.PREFACE 25 MILLS
.COUNT PAGE FROM 1 TO 190 PRINTING "1"
.PAGE←0
.SELECT 1
.NEXT PAGE
.PORTION TITLEPAGE
.GROUP SKIP 5
.BEGIN CENTER
⊗2↓_GIVEN KNOWLEDGE_↓⊗*
⊗5FOR A SYSTEM WHICH WILL DO MATHEMATICAL THEORY FORMATION⊗*
⊗4A System which can develop mathematical concepts intuitively⊗*
.GROUP SKIP 10
⊗5Doug Lenat⊗*
Assisted by Avra Cohn
C. Green, Adviser
Stanford University
Artificial Intelligence Laboratory
This collection of initial knowledge accompanies the THIRD SKETCH of the system
⊗4↓_Not for distribution_↓⊗*
⊗7{DATE}⊗*
.END
.NEXT PAGE
.EVERY FOOTING(⊗7{DATE}, Knowledge for Math Theory Formation, page GIVEN . {PAGE})
.FILL
.AT "⊗2" A "*" ⊂ BEGIN
.TURN ON "{∞→"
.SEND CONTENTS ⊂
⊗7 A* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"
@2A*
.END ⊃
.AT "⊗3" A "*" ⊂ BEGIN
.TURN ON "{∞→"
.SEND CONTENTS ⊂
⊗5A* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"
@2A*
.END ⊃
.PAGE←0
.NEXT PAGE
.NOFILL
.TURN OFF "{"
.INDENT 0
.SELECT 1
.INSERT CONTENTS
.PORTION THESIS
⊗3↓_SECTION 1: OVERVIEW OF BEINGS' FAMILIES_↓⊗*
⊗5and parts present for each family.⊗*
All the parts, with no comments after them
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
DOMAIN/RANGE {not}
ORDERING(Complete)
WORTH
INTEREST
JUSTIFICATION
OPERATIONS
⊗5ACT GROUPING⊗*
CHANGE subgrouping of parts
BOUNDARY-OPERATIONS {not}
FILLIN
STRUCTURE
ALGORITHMS
INTERPRET subgrouping of parts
CHECK
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗5↓_ARCHETYPICAL BEINGS: BEINGS WHOSE NAMES ARE PART NAMES_↓⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES Is this rele. to producing the desired change in the world?
FINAL What situations is this β rele. to bringing about?
PAST Where is this used frequently, to advantage?
IDEN {not}{quick} {fast} tests to see if this β is {not} currently referred to
⊗5ALTER GROUPING⊗*
GENERALIZATIONS What is this a special case of? How to make this more general.
SPECIALIZATIONS Special cases of this? What new properties exist only there?
BOUNDARY What marks the limits of this concept? Why exactly there?
DOMAIN/RANGE {not} Set of (what one can{'t} apply it to, what kind of thing one {never} gets)
ORDERING(Complete) What order should the parts be concentrated on (default)
WORTH Aesthetic, efficency, complexity, ubiquity, certainty, analogic utility, survival basis
INTEREST What special factors make this type of BEING interesting?
JUSTIFICATION Why believe this? For/intu. For thms and conjecs. What has been tried?
OPERATIONS Associated with β. What can one do to it, what happens then?
⊗5ACT GROUPING⊗*
CHANGE subgrouping of parts
BOUNDARY-OPERATIONS {not} Ops rele. to patching {messing}up not-bdy-entities {bdy-entities}
FILLIN How to initially fill it in, when and how to augment what is there already.
STRUCTURE Whether, When, How to retructure (or split) this part.
ALGORITHMS How to compute this function. Related to Repr.
INTERPRET subgrouping of parts
CHECK How to examine and test out what is already there.
REPRESENTATION How should entities of this type be represented internally?
VIEWS How to view as an operator, function, relation, property, corres., set of tuples.
⊗5INFO GROUPING⊗*
DEFINITION Several alternative formal definitions of this concept.
INTU Analogic interp., ties to simpler objects, to reality. Opaque.
TIES Alterns. Parents/offspring. Analogies. Associated thms, conjecs, axioms, specific β's.
EXAMPLES {not} {bdy} Includes trivial, typical, and advanced cases of each type.
CONTENTS What is the value stored here, the actual contents of this entity.
.SKIP TO COLUMN 1
.SELECT 1
⊗5Parts of each archetypical BEING⊗* (one whose name is the name of a BEING part)
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗*
FILLIN
STRUCTURE
CHECK
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
.SELECT 1
.SKIP TO COLUMN 1
⊗5 ↓_OBJECT BEINGS: STATIC HOLDERS OF INFORMATION_↓
Primitive Containers ⊗*
Ordered pair
Variable
Propositional constants
⊗5Structures⊗*
Hist A list which also recalls all past insertions and deletions.
List As in LISP, built out of ordered pairs.
Oset A list with all repetitions of elements disallowed.
Bag A structure with no order, but repetitions are distinct.
Set No order, and no distinct repetitions allowed.
⊗5Assertions⊗*
Axioms True facts which neither have nor need any formal justif.
.SKIP TO COLUMN 1
⊗5 Parts of Object BEINGs ⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
WORTH
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
INTERPRET subgrouping of parts
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
EXAMPLES {not} {bdy}
CONTENTS
⊗5Archetypical BEINGs associated with Object BEINGs⊗*
.BEGIN FILL INDENT 6
Each BEING, indeed each part of each BEING, may point to a special archetypical BEING.
Write B.q.p for part p of the archetypical BEING associated with part q of BEING B.
To save space, to reduce the number of BEINGs which appear in this document, such
information would appear as a new line, labelled p, following the description of
part q of BEING B. For example, just below the description of the Contents of a Set
is a line labelled FILLIN, which explains how to fill in the Contents of a Set.
.END
.SKIP TO COLUMN 1
⊗5↓_ACTIVE BEINGS: DYNAMIC PROPERTIES AND RELATIONS_↓⊗*
⊗5Operation⊗* Transform a given argument into a new entity.
Composition
Insertion
Deletion
Convert-Struc Transform a structure from one type to another.
Substitute
Assign
Mapstruc Replace each member of struc by result of applying given op.
Reverse Ordered Pair
Rule of Inference
Disjunction
Conjunction
Negation
Implication
Unite
Union
Cross-product
Common-parts
Intersection
Setdifference
Put-in-Order
⊗5Relation⊗*
Equality
Membership
Containment
Equivalence
Scope
Quantification
universal: For all
existential: There exists
universally negative: Never
existentially negative: Not always
neither never nor always: For some but not for all
⊗5Property⊗*
Ordered
Extreme
Active.Operations Properties of Active BEINGs.
⊗7NOTE: In actuality, "Relation", "Property", "Operation" are not ACTIVE in any real
sense; they are static meta-entities. For outlining purposes, however, we retain them here.⊗*
.SKIP TO COLUMN 1
⊗5Parts of Relation BEINGs⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
DOMAIN/RANGE {not}
ORDERING(Complete)
WORTH
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
CHANGE subgrouping of parts
BOUNDARY-OPERATIONS {not}
ALGORITHMS
INTERPRET subgrouping of parts
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗5↓_STATIC META BEINGS: OBJECTS WITH JUSTIFICATIONS_↓⊗*
⊗5Statement⊗*
Statement of Generality
Statement of Existence
⊗5Non-justifiable⊗*
Message
Assumption
⊗5Justifiable⊗* but probably unjustified
Conjecture
Bug
Contradiction
Analogy
⊗5Fully justified⊗*
Theorem
Proof
Counterexample
⊗5Mathematica⊗*
Mathematical Theory
Foundation
Basis
Formal System
.SKIP TO COLUMN 1
⊗5Parts of Static Meta BEINGs⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
ORDERING(Complete)
WORTH
INTEREST
JUSTIFICATION
OPERATIONS
⊗5ACT GROUPING⊗*
CHANGE subgrouping of parts
BOUNDARY-OPERATIONS {not}
INTERPRET subgrouping of parts
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗5↓_ACTIVE META BEINGS: ACTIONS WHICH AFFECT BEINGS_↓⊗*
⊗5Inference⊗* Problems to find
Find search a space for a suitable element
Select choose the best element from given alternatives
Guess formulate a new conjecture
Ellipsis infer from examples; and so on; ...
Analogize
Conservation including invariance
Examine prior to attemping pf. or disproof; which is more likely?
⊗5Test⊗* Problems to prove
Assume
Define
Prove
Logically deduce
Prove directly
Cases
Backward chaining
Prove indirectly
Prove statements of generality
Mathematical Induction
Prove statements of existence
Constructively prove existence
Nonconstructively prove existence
Disprove
Constructively disprove
Indirectly disprove
Debug
⊗5Communicate⊗*
With the user
Translation of English
Translation into English
User model
With other BEINGs
⊗5Relation Meta BEINGs⊗* Active Meta-β's which are more relations than ops.
Isomorphism
Categoricity
.SKIP TO COLUMN 1
⊗5Parts of Active Meta BEINGs⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
DOMAIN/RANGE {not}
ORDERING(Complete)
WORTH
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
CHANGE subgrouping of parts
ALGORITHMS
INTERPRET subgrouping of parts
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗5↓_ENVIRONMENTAL BEINGS: MODELS OF SYSTEM FUNCTIONS_↓⊗*
Belief
Interest
Control
⊗7These are probably not going to be BEINGs, but if they are, then here are...⊗*
⊗5Parts of Environmental model BEINGs⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
SPECIALIZATIONS
WORTH
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
EXAMPLES {not} {bdy}
CONTENTS
⊗5↓_Awkward Beings: Those which don't fit in_↓⊗*
These concepts should probably be made into β's or parts-names:
Approximate, Estimate
Level of Detail; Abstraction
Compare
The flow of time: ordering of events
Probability: analogy to geno- and pheno- types in biology (appearance vs internal)
one type is Mathematical probability: expected frequency of a
certain outcome of a repeatable event
one type is Credibility of a single fact whose truth is not yet known
one type is empirical: the observed frequency of a certain outcome
Statistics: We rely on the belief that a sample is in fact representative,
that third type approaches first type approximately.
Mean, median, mode, standard deviation, distributions.
The intuition must include rules for adding mutually excluseive probs,
for multiplying independent probs
To invert: given P(x) and some details about x, fill in the other details.
Any alg for this must yield a consistent x, efficiently.
Uncertainty (Heisenberg) in the world leads to breakdown of absolute prediction.
Randomness. Entropy, dissipation of energy.
.SKIP TO COLUMN 1
⊗3↓_SECTION 2: THE ACTUAL INFO._↓⊗* for each part of each BEING
.SELECT 1
⊗3ANY BEING⊗* Knowledge which is not environmental, yet is common to all.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick} Quick +: mentioned by name. Exact match to definition.
Standard +: Compare current desire to the resons created, when, intu, etc.
Standard -: Examine β's close to this one to ensure that this is ⊗4precisely⊗* what is needed.
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
DOMAIN/RANGE {not}
ORDERING(Complete) {(If a new definition entry has just been created, and it is
not tied to any particular intuition, then the factor in favor of working on
the intuition part next is .95),
(if there are no examples, look for them, .6),
(if a similar new β has just been created, try to find a tie to this one, .6),
(try to find specific specializations (.3), generalizations (.2),
routine ties (.2), and sophisticated ties (.3)),
(boundary elucidation, .1)
(ties: if no ana. and no work ever was done on getting anas., then do so, .6)}
WORTH
INTEREST
JUSTIFICATION
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
STRUCTURE
ALGORITHMS
CHECK
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION
INTU
TIES
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗3ARCHETYPE⊗* BEINGs whose names are also part names. Strategies for part completion.
⊗5RECOGNITION GROUPING⊗* How to know when some part β must be dealt with.
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the β-part of any BEING α.
FILLIN Often, if α is a modified A, then α.β is a similarly-modified version of A.β.
If α is similar to A, with difference D between them, then often α.β will be
similar to A.β, with difference 0 or D or ≤D or (rarely) D'.
⊗5INFO GROUPING⊗* Information about part β, available to all.
DEFINITION Each part name references a body of straegies for dealing with parts of that type.
INTU
TIES Up: BEING in general.
.SKIP TO COLUMN 1
⊗2RECOGNITION GROUPING⊗*
⊗5RECOGNITION GROUPING⊗* How to recognize when the relevant task is to determine rele.
CHANGES {(rele. part goes: unknown to known, .80, .04, intu: piece = rele. part)}
FINAL {(the rele. gp. is Recog), .99, .03, intu: puz. piece wanted is in Recog packet)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the RECOG group of parts of a BEING named β.
FILLIN If one subpart is sparsely enough used, then delete it.
Look at similar β's, try to explicate crucial difference in recognition.
If there is some crucial diff. that always exists wrt. this one, enter in CHANGES/FINAL.
If only vague correlations, enter them in in PAST component.
STRUCTURE Never split. Might restructure if heavily used and very many entries.
Arrange the subparts in decreasing order of (the freq. of usage) * (cost to use)
CHECK Ensure that this β is really distinct from all the rest.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU Several puzzle pieces are needed; β is a packet of pieces; RECOG says when to try them all.
TIES Up: Archtype BEING. Down: Changes, Final, Past, Iden BEINGs.
.SKIP TO COLUMN 1
⊗2CHANGES⊗* Is this rele. to producing the desired change in the world?
⊗5RECOGNITION GROUPING⊗* How to recognize when the relevant part to work on is Changes.
CHANGES
FINAL {(the rele. part is Changes), .99, .03, intu: puzzle piece turns out to be Changes)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the CHANGES part of a BEING named β.
FILLIN The first few times β is succ. used, carefully monitor ⊗4all⊗* changes.
Comb through, each time β is reused, updating probs. for each listed change.
Elim. any entry if its prob. is low and it can't be justified quickly.
Watch especially for Changes mentioned in BEINGs listed in Ties part of β.
STRUCTURE Partition based on types of changes, on prob., and/or on centrality to β.
CHECK Each change should be rare overall compared to its prob.
No prob. should be < 5%.
Any change with prob. < 30% should be justifiable (intui. and/or formal).
REPRESENTATION (change in world, centrality, probability, justification)*
⊗5INFO GROUPING⊗*
DEFINITION The change component reflects a difference in the world which β is rele. to.
INTU
TIES Up: Recog. grouping.
.SKIP TO COLUMN 1
⊗2FINAL⊗* What situations is this β rele. to bringing about?
⊗5RECOGNITION GROUPING⊗* How to recognize when the relevant part to work on is Final.
CHANGES
FINAL {(the rele. part is Final), .99, .03, intu: puzzle piece turns out to be Final)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the FINAL part of a BEING named β.
FILLIN The first few times β is succ. used, carefully monitor ⊗4all⊗* products.
Comb through, each time β is reused, updating probs. for each listed statement.
Elim. any entry if its prob. is low and it can't be justified quickly.
Watch especially for Final products mentioned in BEINGs listed in β.Ties.
STRUCTURE Partition based on types of products, on prob., and/or on centrality to β.
CHECK Each final outcome should be rare overall compared to its prob.
No prob. should be < 5%.
Any entry with prob. < 30% should be justifiable (intui. and/or formal).
REPRESENTATION (future feature or byproduct, centrality, probability, justification)*
⊗5INFO GROUPING⊗*
DEFINITION The Final product component reflects a feature true in the near future,rele. to β.
INTU
TIES Up: Recog. grouping.
.SKIP TO COLUMN 1
⊗2PAST⊗* Where is this used frequently, to advantage?
⊗5RECOGNITION GROUPING⊗* How to recognize when the relevant part to work on is Past.
CHANGES
FINAL {(the rele. part is Past), .99, .03, intu: puzzle piece turns out to be Past)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the PAST part of a BEING named β.
FILLIN The first few times β is succ. used [fails],
extract all int. features of initial sit.
For each, give it a positive weight and put it into the PAST list iff β succeeds;
a negative weight iff β fails; if mixed results, keep the factor but
give it a near-zero weight -- if it recurs mixed, eliminate it eventually.
When reused, update probs. Remove freak entries.
Watch especially for features mentioned in Past part of BEINGs listed in β.Ties.
STRUCTURE Partition based on types of features, on prob., and/or on centrality to β.
CHECK Each situation feature should be rare overall compared to its prob.
No prob. should be < 4%.
Any entry with prob. < 20% should be justifiable (intui. and/or formal).
REPRESENTATION (current feature of world, centrality, probability, justification)*
⊗5INFO GROUPING⊗*
DEFINITION This component makes predictions based on past trends; inference of β's uses.
INTU If it worked once, it'll work again in a similar situation. Treatment as black box.
TIES Up: Recog. grouping.
.SKIP TO COLUMN 1
⊗2IDEN⊗* {not}{quick} {fast} tests to see if this β is {not} currently referred to
⊗5RECOGNITION GROUPING⊗* How to recognize when the relevant part to work on is Iden.
CHANGES
FINAL {(the rele. part is Iden), .99, .03, intu: puzzle piece turns out to be Iden)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the IDEN part of a BEING named β.
FILLIN Initially, with low priority, ask the user how he means to refer to β.
Find ana. β, map over its name. Find sim. β, summarize diff., apply to name.
Whenever β is found relevant, ensure that it and its variations are included.
Imp. to distinguish phrases for β from those for all the BEINGs in β.Ties.
For -: check similarly-referred-to β's, find diffs. in referencing, make explicit.
STRUCTURE Partition based on syn, variat.,freq. of referral, user-name, centrality.
CHECK Each phrase should be rare overall compared to its prob.
No prob. should be < 20%.
Any entry with prob. < 50% should be justifiable (intui. and/or formal).
REPRESENTATION (phrase or word, centrality, probability, justification)*
⊗5INFO GROUPING⊗*
DEFINITION Phrase is English referral to β, esp. by User.
INTU
TIES Up: Recog. grouping.
.SKIP TO COLUMN 1
⊗2ALTER GROUPING⊗*
⊗5RECOGNITION GROUPING⊗* How to recognize when β must alter itself or discuss altering.
CHANGES {(β overall changed, .80, .70, intu: piece = rele. part)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the ALTER group of parts of a BEING named β.
FILLIN
STRUCTURE Might restructure if heavily used and very many entries. Split if high int.
CHECK
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU World sit. is a jigsaw puzzle. These parts are tools to reshape the pieces to fit.
TIES Up: Arch. β. Down: Genl., Spec., Bdy., Dom/Ran, Ordr., Worth, Justif., Ops.
.SKIP TO COLUMN 1
⊗2GENERALIZATIONS⊗* What is this a special case of? How to make this more general.
⊗5RECOGNITION GROUPING⊗* How to know when to generalize β, and how to do it.
CHANGES {(β satisfies ←P(x) instead of ←P(a), .80, closeness of $P to defn. and intu
parts of β, intu: for change: β.intu itself; for prob: resonance/impedance matching)}
FINAL {(Two given concepts are now united in one more general one, .40, .50,
intu: the supersets of the two concepts are equal, containing their union)}
PAST {(the class of entities β encompasses is too small to be int., .95, .90, NIL)}
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the Generalizations part of a BEING β.
FILLIN If β is a specialized form of some α, recast the change from β's point of view.
(Defn, widen, pick any subpart and replace it by a generalization, medium, NIL)
special case: replace a constant by a variable
(Defn, widen, entirely remove one constraint among subparts, medium/low, NIL)
Interesting: when the new boundary (e.g., d/r) is more interesting itself.
STRUCTURE Split off interesting genl.s as new BEINGs, keep other ones here.
CHECK Everything in β.example should fit inside each genl.
∀genl., some bdy. ex. in β.ex. should no longer be on its boundary.
REPRESENTATION (part, change, (how)* , worth, (ptr. to result)* )*
⊗5INFO GROUPING⊗*
DEFINITION A concept x is a genl. of y if x contains all y's plus some other things.
INTU β delimits a set of entities. A generalization delimits a proper superset.
Weaken the concept so as to be able to have it encompass more.
TIES Up: Alter grouping. Opposite: Specializations. Affects: Boundary
.SKIP TO COLUMN 1
⊗2SPECIALIZATIONS⊗* Special cases of this? What new properties exist only there?
⊗5RECOGNITION GROUPING⊗* How to know when to specialize β, and how to do it.
CHANGES {(β satisfies ←P(a) instead of ←P(x), .60, closeness of $P to defn. and intu
parts of β, intu: for change: β.intu itself; for prob: resonance/impedance matching)}
FINAL {(∃ int. new BEING related to β about which new props. may be true, .80, .90,
intu: when throwing stuff out of the β "set", choose to leave an int. core)}
PAST {(the class of entities β encompasses is too large to be int., .95, .90, NIL)}
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the Specializations part of a BEING β.
FILLIN If β is a generalized form of some α, recast the change from β's point of view.
(Defn, narrow, pick any subpart and replace it by int. spec. or ex., medium, NIL)
special case: replace a variable some well-chosen constant
(Defn, narrow, add a new constraint among subparts, medi5m/low, NIL)
If β falls into the category of A∨B∨C∨..., find out which case this one is.
STRUCTURE Split off interesting spec.s as new BEINGs, keep other ones here.
CHECK ∀genl., something in β.ex (esp. bdy. ex.) should no longer fit inside it.
∀genl., some non-bdy. ex. in β.ex. should now be on its boundary.
REPRESENTATION (part, change, (how, worth, (ptr. to result)* )* )*
⊗5INFO GROUPING⊗*
DEFINITION A concept x is a spec. of y if x contains some but (usually) not all y's.
An interesting situation arizes when additional constraints are applied but
the concept surpisingly does not narrow at all.
INTU β delimits a set of entities. A specialization delimits a proper subset.
Strengthen the concept so it will have more power, though encompass less.
TIES Up: Alter grouping. Opposite: Specializations. Affects: Boundary
.SKIP TO COLUMN 1
⊗2BOUNDARY⊗* What marks the limits of this concept? Why exactly there?
⊗5RECOGNITION GROUPING⊗* When is the Boundary part the relevant one?
CHANGES {(β's satisfaction of P switches not quite ↔ just barely, .85, .40, intu:
shifting the boundary of β slightly)}
FINAL {(β can now (not) satisfy P by calling Genl(Spec), .80, .50, intu: shift set bdy.),
(access to the extreme case of β, .80, .55, intu: locate the bdy; op)}
PAST {(the class of entities β encompasses is not quite right to be int, .95, .90, NIL)}
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the Boundary part of a BEING β.
FILLIN Perturb each part briefly, notice whether defn/intu still satisfied. If not,
add: (part, perturbation, {(defn, subpart violated), (intu, opaque)}). If the
defn/intu ⊗4are⊗* still satisfied, this might be a new theorem.
Always look into the fixup if the extended part now includes some new int. things.
Empirically: what do the limits seem to be? THis might lead to conjecture about the bdy.
Intuitively: what do the limits seem to be? THis might lead to conjecture about the bdy.
Formally: can we prove that the boundary is x? contains x? is in x?
Try to reconcile all these opinions by paying them against each other:
For example, if a formal result is unintuitive, find an example empirically.
Especially: if all but one of these views agree, try to find the problem there.
In doing all this, collect hints, algorithms, etc. for finding the boundary
of a BEING like the given one. These may go into its Boundary.Algorithms part.
STRUCTURE ∃ Very diff. thms about diff. subclasses, many int., then split that way.
CHECK Each change component should be a relatively minor change in itself overall.
All together, the bdy. should utilize every scrap of the defn.
REPRESENTATION (part, change, (violation: part, how, temporary/permanent, fixup)* )*
⊗5INFO GROUPING⊗*
DEFINITION Circumstances in which slight perturbations shift entities in/out of β.
INTU β delimits a set of entities. The Boundary demarcates that set's boundary.
TIES Up: Alter grouping.
.SKIP TO COLUMN 1
⊗2DOMAIN/RANGE⊗* Set of (what one can apply it to, what kind of thing one gets)
⊗5RECOGNITION GROUPING⊗* When is the Dom/Ran part the relevant one?
CHANGES {(Way of viewing what this reln. can be applied to and what kinds of things
are produced, .70, .50, intu: the dimensionality of the d+r stays constant)}
FINAL {(β can be applied to a/ β can yield b, .80, .20, intu: any way to do it.)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the Domain/Range part of a BEING β.
FILLIN Initially include (full domain, full range, ptrs. to thms. in β.Ties).
The definition and boundary parts should provide the crossproduct C ⊃ β.
If C = (⊗5X⊗* a b c d ...), choose some dividing point; the head is dom, the tail is ran.
If highly motivated, the ordering of C may be violated (explosive!!).
Once the dom/ran are fixed, decide how (active,set) each is itself to be viewed.
Another way: vary the variables in the defn. until each's bdy. is determined.
Also: if there are many nice examples, guess the domain and range from them.
If the Active is of vast int, or if this same d or r recurs often, name d and r.
STRUCTURE If some entry in CONTENTS of β is more int. than β, let it be a new BEING.
CHECK Examine these ex. eles. of each subdomain, viewed as a set: int, bdy, trivial.
β should apply to each; actually compute the value and store in β.ex.
∀subrange, can each ele. actually be reached?
If too large, try bdy. exs., ensure you can get to disting. eles. of subrange.
If there is no BEING for what you can trim the range to, consider making it one.
For each sdom, find its image in the srange. For each srange, find its preimage in the sdom.
REPRESENTATION (subdom. descr., image descr., (ptr. to special property)* )*
⊗5INFO GROUPING⊗*
DEFINITION Viewing the reln. as over A x B, A is the domain and B the range of β.
INTU View as activity. Can pick any ele. of Domain to work on, will produce ele. in Ran.
The simpler the ⊗4kind⊗* of dom., the more struc. the range must have.
TIES Up: Alter grouping. Assoc: Boundary
.SKIP TO COLUMN 1
⊗2ORDERING⊗*(Complete) What order should the parts be concentrated on (default)
⊗5RECOGNITION GROUPING⊗*
CHANGES {(rele. part to deal with next, .95, .80, intu: itself)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗*
FILLIN Initially, leave blank and let default take over.
If you notice that repeatedly part x is dealt with, fails, then y is
considered, it succeeds, then x succeeds: then include (x,y...). If there
is a contradiction, include special situation factors to distinguish them.
STRUCTURE Keep in sorted in one of the many orderings. Split only when sit.
factors are very big and time-consuming, but partition nicely into sit. classes.
CHECK Use topl. sorting. If no linear ordering exists, ensure that contra. entries
can never be satisfied by the same sit. (disjoint satisfaction sets).
REPRESENTATION (part-name, numerical function)*
The function can apply to parts of the BEING itself, usually the part named
by part-name. It returns a rough estimate of how valuzable it would be to work
on part-name as the next part of this BEING which is COMPLETED.
Notice this implicitly specifies an ordering on all the parts of this BEING.
⊗5INFO GROUPING⊗*
DEFINITION When several parts must be dealt with, which ones are illegal to try next.
INTU Link to next step; linked list; treasure hunt. Anti-links: anything next except...
TIES Up: Alter grouping.
.SKIP TO COLUMN 1
⊗2WORTH⊗* A vector of statistics which are monitored for user, environment, other β.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(β should die now, .30, .10, intu: simply one of the measures)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗*
FILLIN A specific algorithm must be provided here for each component, both for
initially filling it in and for updating it. The initialization of a part
may be from info. present then (which led to its birth), or simply a default value.
Updating functions may be opaque. Perhaps the environment should handle this.
In general: the ⊗4diff.⊗* betw. this and another int. β may be int. in itself.
Look around at the worth componenets of similar and ana. BEINGs.
The diff. betw. β and sim. B. is evaluated and is the diff. in their values, for some component.
Average such estimates over all available similar BEINGs (weight according to similarity).
The aesthetic worth is probably some exponential function of interest and economy.
Analogic utility: how detailed is the intu? how rich and varied and powerful?
STRUCTURE If the Worth of any one part of any β is >> the β, then make a new β for it.
CHECK An efficient, opaque algorithm exists here for each component.
REPRESENTATION (aesthetic worth, overall interest, time efficency, space tied up,
complexity, ubiquity, percentage of success, type of justification,
analogic usefulness, basis for survival/death) ←←notice, no asterisk
Perhaps also: how valuable are its analogues? its consequences? its uses?
How efficient is its representation?
Combine the results of Worth evaluations on all the parts, into some average.
⊗5INFO GROUPING⊗*
DEFINITION Several measures of the performance and character of β.
INTU <the same as the defn, actually>
TIES Up: Alter grouping.
.SKIP TO COLUMN 1
⊗2INTEREST⊗* What special factors make β's interesting?
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(β's interest rating is current, .80, .98, intu: receinving the latest data)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
WORTH Extremely high.
⊗5ACT GROUPING⊗*
FILLIN A specific algorithm must be provided here. The reasoning justifying the
creation shoould provide some entries here; check for duplication with more
general BEINGs' INTEREST parts. If some entry here is a "compiled" form
of a more general interest-factor, that should be noted. Try to do such
preporcessing on each seemingly relevant general interest factor.
If this β is like α(x,y) when x=y, then the interest is extreme:
high if the intuition says it is meaningful/useful, low otherwise.
Updating function may be opaque. Perhaps the environment should handle this.
STRUCTURE Never split. May reorder to speed up average usage time.
CHECK An efficient, opaque algorithm exists here. The later results must agree
with the predictions of the Interest part.
REPRESENTATION (feature, interest weight, origin of this entry and justification)*
⊗5INFO GROUPING⊗*
DEFINITION Features specialized to β's which indicate how interesting instances are.
INTU See intuition for interest in general. Also: compiling more general rules.
TIES Up: Alter grouping. Side: Worth (interest component)
.SKIP TO COLUMN 1
⊗2JUSTIFICATION⊗* Why should one believe this? Formal/intu reasons. Efforts.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(Explicit understanding of how well supported β is, .99, .90, intu: examine)
(Explicit knowledge whether x has yet been tried to esablish β, .90, .99, examine)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗*
FILLIN Whenever anything is tried, record it and evaluate how formal/certain it is.
Initially, some justif. must have been present to nudge BEING creation.
Intu: If a formal proof is found, translate its parts into intus.
Formal: Consider the formal defns. of the entities used in intu. proof. If
a step is small but not quite trivial, use some blind deductive mechanism.
STRUCTURE Separate absolutely certain, formal demonstrations from others.
CHECK Whatever type of reason it is must do the checking. The intu. justif. must
be satisfying as a justif. and as intu. The formal justif. must be valid.
REPRESENTATION (reason, reliability)* Reason can include what has been tried so far.
⊗5INFO GROUPING⊗*
DEFINITION Reasons in support of β.
INTU Pillars physically supporting β. Some are much weaker than others, some could take whole wt.
TIES Up: Alter grouping.
.SKIP TO COLUMN 1
⊗2OPERATIONS⊗* Associated with β. What can one do to it, what happens then?
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the Operations part of BEING β.
FILLIN To determine applicable op., ask relns' and active meta-BEINGs' Dom/Ran parts.
Make sure that the entity is viewed as an object when you do this asking.
If the entity is a whole category of things, see how int. the restricted
op. is (restricted just to this category, this subset of its old domain).
Once op. is known, use general Fillin parts of Changes, Final, Past, Iden BEINGs.
Symbolicly run the op. to try to determine the effects in the case of β.
Often, esp. if the above-derived set is too huge, consider what related and
interesting entity one would like to get out of this, then find an op. which does it.
What can't quite be done to this whole class? Why not? What subclass can it be done to?
Can you change this op. or β slightly so op. ⊗4does⊗* apply to all of β?
What does the op map int. subcalsses of this into?
What are the preimages of int. subclasses of the range? Are ⊗4they⊗* int?
STRUCTURE Interesting to consider β the entire domain of the op.?
Add entry to dom/ran; if int. enough, that arch. BEING will do splitting.
CHECK The operators should all be applicable to each example of β.
REPRESENTATION (op, Recog. grouping for when this op. should be applied to β)
⊗5INFO GROUPING⊗*
DEFINITION Viewed as a static entity, what operations contain β in some subdomain?
INTU Apply operation to β itself.
TIES Up: Alter grouping.
.SKIP TO COLUMN 1
⊗2ACT GROUPING⊗*
⊗5RECOGNITION GROUPING⊗* How to recognize when β must deal with some other BEING α.
CHANGES {(α overall changed, .40, .30, intu: piece = rele. part)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the ACT group of β, which must deal with α.
FILLIN
STRUCTURE Might restructure if heavily used and very many entries. Virtually never split.
CHECK
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU World is a jigsaw puzzle. These parts deal with tools which reshape the pieces to fit.
TIES Up: Arch. β. Down: Interpret subgrouping, Change subgrouping of parts
.SKIP TO COLUMN 1
⊗2CHANGE subgrouping of parts⊗*
⊗5RECOGNITION GROUPING⊗* How to recognize when β must act on some other BEING α.
CHANGES {(α overall changed, .80, .70, intu: piece = rele. part)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the ACT group of β, which must deal with α.
FILLIN
STRUCTURE
CHECK
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU World is a jigsaw puzzle. These parts reshape tools which reshape the pieces to fit.
TIES Up: Arch. β. Side: Interpret subgp. Down: Bdy.ops., Fillin, Struc., Algor.
.SKIP TO COLUMN 1
⊗2BOUNDARY-OPERATIONS⊗*{not} Ops which patch {mess}up not-bdy-entities {bdy-entities}
⊗5RECOGNITION GROUPING⊗* How to recognize when β must act on some other BEING α.
CHANGES {(truth of "α inside β", .90, .50, intu: op = rele. tool)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the ACT group of β, which must deal with α.
FILLIN Create boundary examples first. For each one, examine the part which
changes as the example crosses the boundary. Record what operations can do it.
Consolidate operators.
STRUCTURE Never split. May reorder in order of decreasing frequency of usage.
CHECK Check on examples. Esp: bdy. ex. should change in↔out via a bdy. op.
REPRESENTATION (part, desired change, rele. op., interface)*
⊗5INFO GROUPING⊗*
DEFINITION Operations whose dom. includes α, which map α deliberately into/out of β.
INTU World=puzzle. This part points to the proper tools to reshape the pieces to fit.
TIES Up: Change subgrouping, Act grouping.
.SKIP TO COLUMN 1
⊗2FILLIN⊗* How to initially fill it in, when and how to augment what is there already.
⊗5RECOGNITION GROUPING⊗* When is the rele. part the Fillin part of an archetypical BEING?
CHANGES {(content of part β of some new BEING being filled in, .70, .60, indirect)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* Deal with the FILLIN part of β, which is name of part itself.
FILLIN Think hypothetically: When a BEING is going to be created, what info. of
type β will exist ⊗4then⊗*, but not later, but will be useful later? Put in
a command to save such info. initially. If ever α wishes it had saved some
more β info, modify β's FILLIN part so that next time a β ⊗4will⊗* save this.
CHECK Make sure that the commands are all doable, that each one is used periodically.
REPRESENTATION (situation, command to be followed)*
⊗5INFO GROUPING⊗*
DEFINITION Commands which control what β-type information is kept inside other BEINGs.
INTU
TIES Up: Act grouping, Change subgrouping.
.SKIP TO COLUMN 1
⊗2STRUCTURE⊗* Whether, When, How to retructure (or split) this part.
⊗5RECOGNITION GROUPING⊗* When is the rele. part the Struc. part of an archetypical BEING?
CHANGES {(structure of part β of some new BEING being filled in, .70, .60, indirect)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* Deal with the Struc. part of β, which is name of part itself.
FILLIN Think hypothetically: Can some variable partition a β-type part into many
meaningful subcategories? If so, record the sit. to watch for. Do the higher
up tied BEINGs to β allow splitting? restructuring? Unless some good reason
is actually known, maybe we should leave this blank and let them handle it.
If the same output from a responding part cannot service all kinds of
questioners, then that part should be split, with a suitable repr. for each type.
CHECK Make sure that the β-type parts are not frequently splitting.
REPRESENTATION (kind of restructuring, (sit. where it is called for)* )*
⊗5INFO GROUPING⊗*
DEFINITION Commands which control when the β-type info. in some BEING should be restruc.
INTU When merit threshhold crossed, change the representation of some useful info.
TIES Up: Act grouping, Change subgrouping.
.SKIP TO COLUMN 1
⊗2ALGORITHMS⊗* How to compute (for a relation, some ⊗4doable⊗* entity).
⊗5RECOGNITION GROUPING⊗* When is the rele. part the Algor. part of a BEING?
CHANGES
FINAL {(particular image of particular dom. ele. is known, .90, .90, intu: activity=β)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* Deal with the Algor. part of β.
FILLIN Assemble from the algorithms and defns of each subpart of β.Defn. (inefficient)
Optimize the above out of context as much as possible. Compile (opaque).
Try and rephrase theorems about β so that the algs. can be simplified.
A new repr. may save new info. which can permit great speedups.
STRUCTURE Never split or reorder; can insert a new branch; complete reorg. means new alg.
CHECK Random examinations of applicability and correct results. Esp. bdy. exs.
REPRESENTATION (sequence of steps or compiled name, effic.)*
⊗5INFO GROUPING⊗*
DEFINITION Commands which actually apply the Active β, which get some part of it.
For each element e in the domain of β, this part tells how to compute β(e),
which means how to find {f ε Range(β) | (e,f)εβ}.
The alg. may be recursive, may be nondeterministic, may not be guaranteed to halt.
INTU Instructions for performing some activity. Recipe.
Arrows which take you from starting situation to a new, changed situation.
TIES Up: Act grouping, Change subgrouping. Side: Repr.
.SKIP TO COLUMN 1
⊗2INTERPRET⊗* subgrouping of parts
⊗5RECOGNITION GROUPING⊗* How to recognize when β must examine some other BEING α.
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the Interpret gp of Act gp of β, which must deal with α.
FILLIN
STRUCTURE
CHECK
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION
INTU World is a jigsaw puzzle. These parts examine tools which reshape the pieces to fit.
TIES Up: Act gping. Side: Change subgping. Down: Check, Repr., Views parts.
.SKIP TO COLUMN 1
⊗2CHECK⊗* How to examine and test out what is already there.
⊗5RECOGNITION GROUPING⊗*
CHANGES (empirical belief in β, .30, .90, intu: coincidences are rare)
FINAL
PAST (if x→y is known, y is less intu. than x, then check y instead of x,.50,.60,)
IDEN {not}{quick}
⊗5ACT GROUPING⊗*
FILLIN Is there some independent way to get (some of) the same results as this?
The sit. is typically "initially" or "periodically".
ALGORITHMS Check a less likely corollary; check it outside the range of intuition
CHECK If check indicates ERROR, then doublecheck how the test was derived before failing.
REPRESENTATION (sit, command to be followed)*
⊗5INFO GROUPING⊗*
DEFINITION
INTU If two routes should both lead to same result, take both and compare results.
TIES Up: Interpret subgp., Act group
.SKIP TO COLUMN 1
⊗2REPRESENTATION⊗* How should entities of this type be represented internally?
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(how β is represented internally), .99, .95, intu: direct)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗*
FILLIN Default: examine tied BEINGs' representations for suitability.
Especially, this must be efficiently compatible with those which it interacts with.
Clever algorithm to decide on a good new representation: ...
take into account what kinds of things must be saved,
what types of duties it must perform, what questions it must answer,
what parts of the initially chosen repr. are dont-cares (can manip. them),
what theorems or known properties of this concept allow computational shortcuts.
STRUCTURE If much of the struc. is wasted (in the sense that all of it is needed
for some entry or other, but no single entry uses more than a small % of it)
then split into subclasses, where each has a much simpler repr.
<This might need much more elaboration, new ideas here, etc.>
CHECK All imp. info. to be saved has a place to be saved specified in the repr.
REPRESENTATION Description in formal type 3 language, which employs standard
symbols (,[]{}*+) and additional limited ones :<>change, part, sit, prob, %,...
⊗5INFO GROUPING⊗*
DEFINITION The internal format, the prototypical syntax, of β.
INTU Etiquette; uniformity; agreement in advance to simplify interface.
TIES Up: Interpret subgp., Act group
.SKIP TO COLUMN 1
⊗2VIEWS⊗* How to view any β as a type of α. (e.g., a relation viewed as an object)
⊗5RECOGNITION GROUPING⊗*
CHANGES {(what kinds of things β is suited for, .60, .70, intu: indirect)}
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the Views part of β.
FILLIN Default: examine tied BEINGs' views for suitability.
Can ⊗4always⊗* view as an object; often as a relation as well: ask them.
Also ask other BEINGs if they can view this entity differently.
STRUCTURE If two views have very different interesting thms, slight grounds for split.
CHECK ∀view, some ex. is well-represented in that view. ∀ex, some view is suited.
REPRESENTATION (view, tie to other BEING, (other view, transformation details)* )*
⊗5INFO GROUPING⊗*
DEFINITION Equivalent formulations of the same concept β.
INTU The way you look at something affects how easily a given task can be done to it.
TIES Up: Interpret subgp., Act group. Side: Representation
.SKIP TO COLUMN 1
⊗2INFO GROUPING⊗*
⊗5RECOGNITION GROUPING⊗* How to recognize when to simply grab onto some ∃ info.
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the RECOG group of parts of a BEING named β.
FILLIN
STRUCTURE
CHECK
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Static facts, organized for easy access by others.
INTU Static facts, organized for easy access.
TIES Up: Archtype BEING. Down: Defn, Intu, Ties, Exs, Contents.
.SKIP TO COLUMN 1
⊗2DEFINITION⊗* Several alternative formal definitions of this concept.
⊗5RECOGNITION GROUPING⊗* When is the Definition the rele. thing to deal with?
CHANGES
FINAL {(aware exactly of constraints on β, .90, .90, intu: consultation)}
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the definition part of a BEING.
FILLIN Initially supplied by user or by STRUCTURE part of a BEING who is tied upward.
Typically, conjoin some additional constraint (or remove one) from another β's defn.
If x is used frequently or is interesting, a definition becomes a necessity.
CHECK ∃ at least one entity satisfying the definition.(put it in ex. part)
The "truth" or belief in a definition, its justif, is by absolute assumption,
hence neither can nor should be "checked" in any way except intuition.
Eliminate redundant constraints from the defn: independence: those remaining imply the others.
There must be no circularity, no recursions that do not progressively get simpler.
The justification for a recursive definition of an infinite entity includes the
assumption of the principle of choice; if this is not in foundation, insert it.
REPRESENTATION (descr. in formally usable terms, (part, most rele. entry there)* )*
⊗7Note: possibly, all the Axioms which appear in the definition parts should really be put in the Ties part.⊗*
⊗5INFO GROUPING⊗* Static facts about the definition parts of BEINGs.
INTU The ultimate authority; the rules of the game. View β as a set; defn. is then
the specification of its characteristic function; testing for satisfaction is
then like using the Membership function.
This part can contain things to substitute for the concept, things which tell
you recursively whether or not something is in this concept, special terms for variants.
TIES Up: Info group
.SKIP TO COLUMN 1
⊗2INTU⊗* Analogic interp., ties to simpler objects, to reality. Opaque.
⊗5RECOGNITION GROUPING⊗* When is the Intuition the rele. thing to deal with?
CHANGES
FINAL {(aware quickly of some facet of β in action, .80, .70, intu: apply)}
PAST {(contradiction, .30, .30, intu: let intus. explain the problem)}
IDEN {not}{quick}
⊗5ACT GROUPING⊗* How to deal with the intuition part of a BEING.
FILLIN Assemble the translations of the subparts of the Definition into intuitions
of compatible formats. The combination-words in defn. become top-level fns.
Important: must fill in how each intu. is tied to its corr. definition.
If the definition temporally succeeds the intuition, then ask the intu. for
alternative views, for rippling waves of more and more distant images;
simultaneously, obtain several alternative intuitions directly from the new defn.;
keep up until activator is too low or until some nontrivial ∩.
Then keep only the intuitive tie-in and perhaps a few of the direct intuitions.
CHECK Each example makes sense intuitively. Lower priority: each part makes sense.
REPRESENTATION (name, how to call it, use, reliability, ptr. to most rele. defn, how tied)*
⊗5INFO GROUPING⊗* Static facts about the intuition parts of BEINGs.
DEFINITION Opaque functions which can simulate an actual real microworld, incl. β.
INTU The ultimate authority; the rules of the game.
TIES Up: Info group
.SKIP TO COLUMN 1
⊗2TIES⊗* Alterns. Parents/offspring. Analogies. Associated thms, conjecs, axioms, specific β's.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick} also encompasses assimilation
⊗5ACT GROUPING⊗*
FILLIN The ties are filled in as they become known; only small work initially.
In general, use intuition to ripple out to other intuitions; use anas.
The up ties are known at conception.
The down ties are those down ties of the upward BEINGs which still hold.
Analogies with β as one component should be sought.
Seek thms. and conjectures about β, also involving other BEINGs perhaps.
Examples suggest conjecs, conjecs lead to thms, pat-matching leads to alt.
Expand the set which was found in ths way, by looking at ⊗4their⊗* ties, spec, genl.
There may be a v. effic. repr. of β in terms of some other BEING + some difference.
STRUCTURE Any with high interest are split off as new BEINGs freely.
If the tying relnship. is nonspecific, the new β is os type Analogy;
if the tie is a specific relation R, but the arguments are general, a new Conjecture;
if the tie R is specific and the arguments are, too, then create a new example
of a pair in the <tie> relation, i.e., a new entry in R.EXAMPLES.
CHECK Is this consistent, esp. with intution. Technically, must be, too, with defn.
REPRESENTATION (relnship./difference, (name, optional details)* )* , where
the known relationships are up, down, side, analogies + the work done to
find analogies, thms, conjecs, relevant axioms, alternatives.
⊗5INFO GROUPING⊗*
DEFINITION Other BEINGs which are related to β in an interesting way.
INTU Neighbors, relatives.
TIES Up: Info group. Side: Ana., Thm., Conjec., Exs., Family-structure.
.SKIP TO COLUMN 1
⊗2EXAMPLES⊗* {not} {bdy} Includes trivial, typical, and advanced cases of each type.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ACT GROUPING⊗*
FILLIN Specialize β (in various ways) until only one entity is specified.
Any kind: instantiate specializations, and/or defn, and/or intu.
Inefficient: scan related specific entities until an ex. is found
also: look for op. F: α→β; then use f(α.Examples).
Consider ana. β's examples, map them back. Examine similar β's exs.
Special: To get an example that satisfies P, bear P in mind at each spec. choice point.
Try setting various parameters s.t. they are equal to each other.
Simplest: plug in simple distinguished concepts into defn/intu. until singleton.
Consider the trivial case, the empty or minimal extreme, the base step of a recursive defn.
Big: Plug sophisticated, big, varied examples of each variable concept into defn/intu.
If recursive, try to invert it so as to be able to build up harder and harder exs.
Done: only use it to find a few actual examples.
Save the inverted procedure for later usage, though.
Pick some decent example, find a chain of simpler and simpler examples
leading backward, then turn around and extrapolate off the hard end.
Prototypical: so representative that they will be useful in the future for
testing a conjecture for empirical plausibility.
Potentially: formally prove that any tie to this ex. is a valid tie.
Boundary: keep an eye out for two similar examples, one in and the other out.
(these can come from work on this part and/or from similar B's exs.)
When such a pair is found, begin transforming them into each other,
and zero in on the most similar pair of in/out entities. Examine carefully.
Afterwards: if ¬∃ exs. before, ∃ exs. now, ∃ op O on β with no O.Exs, then
place into O.Exs. this suggestion: can plug eles. of β.Exs into O.
STRUCTURE Split off any indiv. or class of high-int. examples, keep the rest here.
CHECK Each ex. should satisfy the defn. and intu parts.
If any type of new procedure (e.g., inverted recursive defn) has been created,
which supposedly generates β's, try to conjecture about the uniqueness of the
members of the sequence produced, the totality of their covering of all possible β's, etc.
REPRESENTATION (name, type, (part present, value, change from β)*, origin, complexity,
distance from the boundary of β)*
Data about examples should be stored under part headings (easy to make them BEINGs).
The types of type are: +, + boundary, -, - boundary.
The types of origin are: by specializing defn, by intu, to satisfy property.
⊗5INFO GROUPING⊗*
DEFINITION Specific entities which are (not)(barely) instances of β's.
INTU Zero in on specific representatives, individuals.
TIES Up: Info group. Side: Specializations.
.SKIP TO COLUMN 1
⊗2CONTENTS⊗* What is the value stored here, the actual contents of this entity.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(β was actually used, .60, .40, intu: apply)}
PAST
IDEN {not}{quick} actually evaluate
⊗5ACT GROUPING⊗*
FILLIN Specified by the Fillin part of β, if it has one. Else construct from defn.
Also here should go a tag as to what kind of handle this has (nonconstruc ∃,
construc. ∃, reasonable algorithm, pointer to satisfying concrete entity).
CHECK Should satisfy defn., encompass all examples, satisfy intu.
REPRESENTATION This is specified by the repr. part of β, augmented by a handle-quality tag.
⊗5INFO GROUPING⊗*
DEFINITION The actual specific entity which is defined and constrained in the other parts.
INTU The value of a variable named β; the actual information at the end of a search.
TIES Up: Info group.
.SKIP TO COLUMN 1
⊗3OBJECT⊗* Static holders of information.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
SPECIALIZATIONS {(defn, addl. contraints on subparts, v. good, structure),
(intu, fundamentality, good, axiom)}
BOUNDARY {(operations, include EVALUATE, (intu, no longer static)),
(justification, needs to be filled in, (justif, no longer absolutely basic))}
WORTH (.5, .4, .6, .6, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST {(repr. is s.t. operations can be done to it efficiently, .8, efficiency),
(its subparts are related in some way other than just by ε this object, .9, int)}
OPERATIONS Access
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Static holder of information.
INTU A receptacle for objects, a container.
TIES Up: Specific-Knowledge-BEINGs BEING
EXAMPLES {not} {bdy} Bdy: Relation. -Bdy: Communicate
CONTENTS
.SKIP TO COLUMN 1
⊗2ORDERED PAIR⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(representation, length, (nested, v. good, list))}
SPECIALIZATIONS {(representation, order, (remove, good, pair or doubleton set))}
BOUNDARY {(repr, constraints on each component to encode a structure, (intu, pairness)),
(arg, both components are equal to x, blah,, same informational content as {x})}
WORTH
INTEREST
OPERATIONS {(Reverse: switch the ordering of the elements),
(replace first (second) ele. by this given value),
(access first (second) element of the ordered pair)}
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION (first element, second element) i.e., (element)2 in order
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Two pieces of information plus the notion of one preceding the other.
Alternate: an element of the cross-product of two given sets.
Alternate: encoded into a set as (a,b) = {a,{a, b}}.
Alt: a set s = {a,b} = (CLASS a b) and a variable named Front↓S whose value
is either a or b. PEQUAL thus means Set-equal, plus the equality of the Front variables.
An ordered pair is a list P satisfying these constraints:
CAR(P) = "PAIR"
CDDR(P) ≠ NIL
CDDR(P) = NIL
CADR of the list structure is called the first element of P, FIRST(P).
CADDR of the list structure is called the last element of P, LAST(P).
There is no recursive definition of an ordered pair.
Two pairs are equal, PEQUAL, iff FIRST of each are equal, and LAST of each are equal.
Considering both first components as type x structures, the equality test
on the two first components is the x-type-equal test. Sim. for last elements.
For example, if the pairs have a bag as first ele. and a set as last ele., then
PEQUAL(P,Q) ↔ BAG-EQUAL(FIRST(P), FIRST(Q)) ∧ SET-EQUAL(LAST(P), LAST(Q)).
To insert e as the first element of a pair S, call INFIRST(e, S).
To insert e as the last element of a pair S, call INLAST(e, S).
To merely access the first element of a pair S, call FIRST(S).
To merely access the last element of a pair S, call LAST(S).
To test whether two pairs S,R are equal, call PEQUAL(S, R).
(For readability, below, PEQUAL is abbreviated ==, its negation is ≠≠.)
To indicate that FIRST and LAST are functions, we might say:
∀x,y,∀pair P. ELEMENT(x, FIRST(P)) ∧ ELEMENT(y, FIRST(P)) → x=y.
For this reason, we shall write FIRST(P)=x, when we really mean ={x}.
These four relations satisfy the following conditions:
∀e.∀pair P. e = FIRST(INFIRST(e, P))
∀e.∀pair P. e = LAST(INLAST(e, P))
∀e.∀pair P. FIRST(P) = FIRST(INLAST(e,P))
∀e.∀pair P. LAST(P) = LAST(INFIRST(E,P))
∀pair P. P == INFIRST(FIRST(P), P)
∀pair P. P == INLAST(LAST(P), P)
∀e,f.∀pair P. INLAST(e, INFIRST(f, P)) == INFIRST(f, INLAST(e, P))
∀pairs P,Q. P == INLAST(LAST(P), INFIRST(FIRST(P), Q))
∀pairs P,Q. P==Q ↔ (FIRST(P)=FIRST(Q) ∧ LAST(P)=LAST(Q))
INTU Envelope holding some info and also another envelope which holds some info.
(a,b) can be viewed as a vector from (0,0) to (a,b) in the plane, its length
and its direction known; intuitively understand vector operations (+,x,.)
TIES Up: List, Cross-Product. Down: Doubleton
EXAMPLES {not} {bdy}
CONTENTS
FILLIN
.SKIP TO COLUMN 1
⊗2VARIABLE⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Pointer, object, entity
SPECIALIZATIONS {(second componenet, restrict what class of things in which it may
legally point)}
BOUNDARY {(value is irrelevant, named object only),
(name is irrelevant or unknown, same as nonexistence),
(value is unknown, points to default value, e.g. "NOBIND"),
(name is same as value, variable is indistinguishable from what it points to)}
WORTH (.5, .4, .6, .5, .5, .6, .6, (1.0 formal, .7 intu), .6, (1.0 basis))
INTEREST A single statement, containing a variable, can represent ∞ of similar statements.
Say only the ⊗4kind⊗* of value of an entity is known (say it is of type K), but we
don't know its specific identity; then one may pick any new name, say n,
assume that n is of type K (e.g., nεK), and assume that n is one name for our entity.
OPERATIONS Access the value, assign, quantify;
use this variable's name in place of the kind of thing its value is.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION (name, value)
VIEWS (as an ordered pair (name, value))
(as a pointer labelled <name> pointing to <value>)
(as one pair in an operation called VALUE-OF, with VALUE-OF(name)=value)
(as an operation named <name> with no argument, whose result is value)
(as a predicate named <name> over the space of possible values, with the constraint
that only one is T at any time.)
(as a constant, where for any given usage (typically a statment) it always means <val>)
⊗5INFO GROUPING⊗*
DEFINITION Named holder of information. Each occurrence indicates the same info,
unless an intervening form has re-assigned this variable somehow.
Two variables are assumed to be equal if their names coincide.
Two variables can be proven to be equal by showing that their values coincide;
in this case, we write name↓1 = name↓2; "=" means variable-equality.
Different names do not necessarily imply that the variables have different values.
(Two variables with the same value may have different names).
INTU A named receptacle for an entity. A container with a label and a contents.
An arrow with a label and a target; or: with a named start and a target.
The name of a person and his physical body. One person may have several "names"
he recognizes (depending on the caller and the situation), and many of
these he shares with other people (eg, "hey, you!").
TIES Up: Object
EXAMPLES {not} {bdy}
CONTENTS One might view the contents of a variable named N to be the value V.
.SKIP TO COLUMN 1
⊗2PROPOSITIONAL CONSTANT⊗* Basic concept of simple true and false values.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Theorem, Conjecture, Propositional-valued variable
SPECIALIZATIONS
BOUNDARY (identity is unknown, propositional-valued variable or conjecture)
(structure is complex even though value is known, theorem)
WORTH (.5, .1, .7, .1, .1, .6, .5, (1.0 formal, .8 intu), .3, (1.0 basis))
INTEREST A statement (a variable with a big name whose value is a propositional constant)
, is uninteresting if it is vacuous, trivially true or false, its value is obvious.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION the atom T or F, or a form which evaluates to same.
VIEWS (as the absolute extremes of belief)
(as the set which all predicates call their range)
(as the set into which (dis)prove causes the belief in a conjecture to point)
⊗5INFO GROUPING⊗*
DEFINITION A primitive piece of information, a stae of the truth of an entity.
INTU The ultimate (positive or negative) belief value; reliable or reliably false.
Related to the always and the never quantifications.
Truth and falsity are determined semantically, based on whether or not the given
statement holds in (the current model of, interpretation for) the real world.
TIES Up: Object, Variable, Belief, Proof/Counterexample
EXAMPLES {not} {bdy} T (true), F (false)
CONTENTS The contents are really indistinguishable from the name.
.SKIP TO COLUMN 1
⊗2STRUCTURE⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(info. present is organized together, .70, .95, intu: do the puzzle)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(defn, addl. constraints, (recall each change in order, poor, hist)
(recall current state after all changes, v. good, bag),
(recall curr. state and order of insertions into structure, v. good, list),
(never accept already-present member, v. good, set))}
BOUNDARY {(operations, any removals, (defn and intu, no longer same( (worth, lower))}
WORTH (.5, .4, .6, .6, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST {(repr. is s.t. operations can be done to it efficiently, .9, efficiency),
((quan)x in struc, P(x) holds, sqrt(interest of this property*int. of quan.))}
OPERATIONS {(INSERT: accept a new member for this structure,),
(DELETE: consider a request to remove a member, Past: the memb. must be net present),
(ACCESS: how to get some member of the structure (perhaps some special member)),
(SUBSTRUCTURE: how to tell if one structure is technically a substructure of another),
(MEMBERSHIP:answer whether a specific element is net present or not),
(EQUALITY: answer whether two given structures are equal),
(CONVERT: Take a structure which is of type x and view it as if it were of this type)}
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Static organizer and holder of related information.
CHECK: Any entity with component parts and constraints upon them.
FILLIN: Look for intu. ties betw. all the operations, then postulate them.
INTU The pieces of info. are like pieces of a jigsaw puzzle. Or:
A blob whose nucleons oscillate in legal modes.
FILLIN: Any intu. constructs which seem to just satisfy the defn.
TIES Up: Object
EXAMPLES {not} {bdy}
FILLIN: apply Convert-struc. to exs. of other types of structures than the given one.
In such situations, perhaps it is good to keep a ptr. to what each cam from.
Also: to get an int. example, try conjoining (some of) the Interest
parts' (of up↑*(B)) suggestions as addl. constraints onto the defn.
CONTENTS Members in the structure; possibly also accepted requests for deletions.
.SKIP TO COLUMN 1
⊗2HIST⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(defn, addl. constraints,
(recall (unordered) non-negatd acceptances, v. good, bag),
(recall non-negated acceptances in order of their insertion, v. good, list),
(never accept already-present member and disregard order, v. good, set))}
BOUNDARY {(operations, any removals, (defn and intu, no longer same( (worth, lower))}
WORTH (.3, .2, .3, .7, .7, .1, .8, (1.0 formal, .6 intu), .1, (1.0 basis))
INTEREST
OPERATIONS {(answer a request if a given element was ever inserted/deleted before
a second given element was inserted/deleted)}
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION ((insert/delete, name of member)* in order)
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Recall in order every acceptable request made to insert or delete ele. of struc.
Recursively: A Hist H is NIL or an ordered pair (e, J), where J is a Hist and
e is itself an ordered pair (op, d), where d is an object and op is either
the word H-INSERT or the word H-DELETE. A turing-machine-like algorithm is
provided for scurrying back and forth, cancelling out requests to add and
to delete a given element; this is used to see if that ele. is still "net in"
the Hist or not. If it is, then a DELETE request can be entered. An INSERT
request can ⊗4always⊗* be entered. No record is kept of unsucc. requests.
INTU The pieces of info. are like pieces of a jigsaw puzzle.
TIES Up: Structure.
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: In order, record each transaction.
.SKIP TO COLUMN 1
⊗2LIST⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(structure goes unordered→ordered, .60, .60, intu: arrange (intu struc))}
FINAL
PAST
IDEN {not}{quick} tuple, vector, ordered bag
⊗5ALTER GROUPING⊗*
GENERALIZATIONS (ops, addl. ability, (recall all accepted transactions, poor, hist))
SPECIALIZATIONS {(defn, addl. constraints,
(no order is recalled, v. good, bag),
(no order and also never accept already-present member, v. good, set)),
(length, restricted, (to a pair, v. good, ordered pair))}
BOUNDARY {(operations, any addn/remov., (defn and intu, no longer same( (worth, lower)),
(specific extremes of any list: first element of a list, last element)}
WORTH (.6, .7, .7, .6, .5, .8, .8, (1.0 formal, .8 intu), .8, (1.0 basis))
INTEREST
OPERATIONS {(Member: answer a request if a given element is present),
(equality test: the cars are equal and the cdrs are equal),
(sublist: test whether x is a sublist of y)
(CAR:access the last element which was inserted)}
(CDR:access what the list would be if the last inserted element were removed))}
(not invariant: delete an element from a list which contains it)
(not invariant: change the order of the elements of a list)
(not invariant: insert any element into any list)
Prove: prove true for bags, then prove that ordering is preserved.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(order part of defn, satisfied, LIST, feed eles.in order),
(order part of defn, satisfied, SORT, provide general rule for deciding precedance)}
REPRESENTATION ((name of member)* in order) Pragmaticly: a LISP List structure.
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Recall in order every accepted element which was never deleted.
Only the ⊗4relative⊗* order is recalled, not any absolute ordering value.
Recursively: A list L is either NIL or an ordered pair (e, S), where
e is an object and S is a list. e is called the front element or CAR of L.
S is called the remainder or CDR of L. If S=NIL, then e is called the
last element of L. If S≠NIL, then the last element of L is defined to be
the last element of S. S is a tail of L, as is each tail of S. The
elements of L include precisely e and all the elements of S. NIL has no eles.
Recursively: NIL is a list. So is the result of CONS(e,L) where L is a list.
The elements of CONS(e,L) are e and all elements of L. NIL has no elements.
There are no other entities called lists or elements of lists.
Two lists are equal (EQUAL, =) iff either they are both NIL or else
their CARs are both equal, and their CDRs are both EQUAL. The equality of the
CARs is generally performed using EQUAL, but if they are to be viewed as
some other type x of structure, then one could agree to use the x-equality test.
To insert an element e into a list S, replace S by CONS(e, S).
To delete the first element of a list S, replace S by CDR(S).
To test whether x is an element of S, call MEMBER(x, S).
To test whether two lists S,R are equal, call EQUAL(S, R).
To test whether list R is a sublist of list S, call SUBLIST(R,S).
To merely access the first element of a list, call CAR(S).
To hypothetically examine what the list would be like without its CAR, call CDR(S).
To hyp. examine what list would be with new front ele. e, call CONS(e,S).
∀x.∀y. MEMBER(x,y)={T}∨ MEMBER(X,Y)={F}. So we abbreviate {T} as T below, etc.
Another view: T abbreviates {T}, F abbreviates any of PHI,{F},{T,F}.
For example, we say: ∀x.∀y. MEMBER(x,y) = T or MEMBER(x,y) = F.
These relations satisfy the following conditions:
∀e.∀list S. MEMBER(e, CONS(e, S)) = T
∀e.∀list S. e = CAR(CONS(e,S))
∀e.∀list S. MEMBER(e, S) ↔ (e=CAR(S) or MEMBER(e,CDR(S)))
∀e. MEMBER(e, NIL) = F.
∀list e. MEMBER(e,e) = F.
∀list S≠NIL. S = CONS(CAR(S), CDR(S))
∀list S≠NIL. S ≠ CDR(S)
∀list S.∀e. S ≠ CONS(e, S)
∀lists S,R. SUBLIST(R,S) ↔ R=NIL or (S≠NIL ∧
((CAR(R) = CAR(S) ∧ SUBLIST(CDR(R),CDR(S))) or SUBLIST(R,CDR(S))))
∀lists S,R. S=R ↔ (CAR(S)=CAR(R) ∧ CDR(S)=CDR(R))
From the above two it might be hard to prove that "=" is just sublist both ways.
NIL = NIL
Although Interlisp sets Car and Cdr of NIL to NIL, the system won't know that.
INTU Stack of trays, queue of waiting people, string of characters, tower of blocks.
TIES Up: Structure.
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Insert elements in order, starting with the last one first,
into NIL, by calling CONS of new element and current list.
To fill from front to rear, use NCONC1 of list and new ele.
.SKIP TO COLUMN 1
⊗2OSET⊗* An ordered set; a list with no repetitions of elements.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS List, Ordered Pair
SPECIALIZATIONS Set
BOUNDARY
WORTH (.2, .3, .6, .5, .4, .1, .4, (1.0 formal, .5 intu), .5, (1.0 basis))
INTEREST (some property exists tying the elements together besides membership, .9)
OPERATIONS {(membership: answer whether a given element is present or not),
(=: are two given osets equal: membership question always gives same ans.),
(CAR: access the front member of the oset),
(suboset: test whether x is a suboset of y),
(make an element present (until its next deletion)),
(make an element not present (until the next insertion))}
Prove: Prove it true for sets, then show that ordering is preserved.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION ((name of member)* in order, no repetitions)
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Recall every element which has not been deleted since it was inserted,
in the order in which it was last successfully inserted (change in oset).
An oset S is a list whose CAR is "OSET".
CADR of the list structure is called an element of S.
When the CADR is deleted from S, the result W is called a tail of S.
Any tail of W is also called a tail of S.
Any element of W is also called an element of S.
The OSET constraint is that no two elements may be equal. Also, two
OSETs are not equal unless their elements and their order coincide exactly.
Recursively: the list (OSET) is an oset, called the empty oset OPHI.
If S is an oset, then so is (OSET-INSERT e S), and e is called an element of S.
There are no other entities called osets; there are no other elements of S.
Two osets are equal, OSET-EQUAL, iff either they are both OPHI or else
CAR of each is equal and CDR of each is equal. CAR of an oset is its first
element, CDR is what is left when that is deleted.
To insert an element e at the front of an oset S, call OSET-INSERT(e, S).
To delete the front element e from anosetg S, replace S by CDR( S).
To access the front element e of an oset S, call CAR(S).
To access all but the front element e of an oset S, call CDR(S).
To test whether x is an element of S, call OSET-MEMBER(e, S).
To test whether oset R is a suboset of oset S, call SUBOSET(R, S).
To test whether two osets S,R are equal, call OSET-EQUAL(S, R).
∀x.∀y.∃1zε{T, F}. OSET-MEMBER(x,y)={z}. So we abbreviate {T} as T below, etc.
Above, ∃1 is an abbreviation for saying that only {T} and {F} are possible values.
These relations satisfy the following conditions:
OSET-MEMBER is identical to LIST-MEMBER
if x is a member of S, then OSET-INSERT(x,S) = S; else it equals CONS(x,S).
OSET-EQUAL is identical to LIST-EQUAL (=)
CAR and CDR are the same as the list functions CAR, CDR.
SUBOSET is identical to SUBLIST
OPHI is the list (OSET) and satisfies all the analogous properties as the list NIL.
Thus the only difference between lists and osets is that trying to CONS
on an already-present element is not allowed (has no effect on the oset).
INTU Hard to imagine; rarely used in programs or in mathematics.
Provide intu. for each oset operation: member, insert, delete, equality, suboset.
TIES Up: Structure.
EXAMPLES {not} {bdy}
CONTENTS elements, no repetitions
.SKIP TO COLUMN 1
⊗2BAG⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(ops, addl. ability, (recall all accepted transactions, poor, hist),
(recall order of insertion of present elements, good, list)
(number of deletions must at least equal no. of insertions before removal, good, bag)}
SPECIALIZATIONS
BOUNDARY {(operations, any addn)remov., (defn and intu, no longer same( (worth, lower))}
WORTH (.8, .8, .7, .5, .4, .99, .9, (1.0 formal, .8 intu), .8, (1.0 basis))
INTEREST (some property exists tying the elements together besides membership, .9)
OPERATIONS {(membership: answer awhether a given element is present or not),
(=: are two given bags equal: membership question always gives same ans.),
(some-member: access a member of the bag),
(subbag: test whether x is a subbag of y),
(make an element present (until its next deletion)),
(make an element not present (until the next insertion))}
(invariant: order it (convert to a list), change order, reconvert to a bag)
(not invariant: delete an element form a bag which contains it)
(not invariant: insert any element into any bag)
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION ((name of member)* not in any particular order)
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Recall every element which has not been deleted since it was inserted.
A bag S is a list whose CAR is "BAG".
CADR of the list structure is called an element of S.
When the CADR is deleted from S, the result W is called a tail of S.
Any tail of W is also called a tail of S.
Any element of W is also called an element of S.
The BAG constraint is that two elements may be equal, but order of insertion is never rele.
Recursively: the list (BAG) is a bag, called the empty bag BNIL.
If S is a bag, then so is (BAG-INSERT e S), and e is called an element of S.
There are no other entities called bags; there are no other elements of S.
Two bags are equal, BAG-EQUAL, iff either they are both BNIL or else
one contains e as an element and the results of BAG-DELETing e from each
structure are two new bags which are BAG-EQUAL.
To insert an element e into a bag S, call BAG-INSERT(e, S).
To delete an element e from a bag S, call BAG-DELETE(e, S).
To access some element e of a bag S, call SOME-BAG-MEMBER(S).
To test whether x is an element of S, call BAG-MEMBER(e, S).
To test whether bag R is a subbag of bag S, call SUBBAG(R, S).
To test whether two bags S,R are equal, call BAG-EQUAL(S, R).
(For readability, below, BAG-EQUAL is abbreviated ==, its negation is ≠≠.)
∀x.∀y.∃1zε{T, F}. BAG-MEMBER(x,y)={z}. So we abbreviate {T} as T below, etc.
For example, we could say: ∀x.∀y. BAG-MEMBER(x,y) = T or BAG-MEMBER(x,y) = F.
These six relations satisfy the following conditions:
∀e.∀bag S. BAG-MEMBER(e, BAG-INSERT(e, S)) = T
∀e.∀bag S. S == BAG-DELETE(e, BAG-INSERT(e, S))
∀e.∀f≠e.∀bag S. BAG-MEMBER(e, BAG-INSERT(f, S)) = BAG-MEMBER(e, S)
∀e.∀f≠e.∀bag S. BAG-MEMBER(e, BAG-DELETE(f, S)) = BAG-MEMBER(e, S)
∀e.∀bag S. S ≠≠ BAG-INSERT(e, S)
∀e. BAG-MEMBER(e, BNIL) = F
∀e.∀bag S. BAG-MEMBER(e, S) → S≠≠BAG-DELETE(e, S)
∀non-BNIL bags S,R. S==R ↔ (∀e. BAG-MEMBER(e, S) = BAG-MEMBER(e, R) and
BAG-DELETE(e, S) == BAG-DELETE(e, R))
∀e. BAG-DELETE(e, BNIL) == BNIL.
∀bag S. SUBBAG(BNIL,S) = T
∀bags R,S. SUBBAG(R,S) = (R=BNIL or ∀e.(BAG-MEMBER(e, R) →
(BAG-MEMBER(e, S) ∧ SUBBAG(BAG-DELETE(e,R), BAG-DELETE(e,S))
∀bag S≠BNIL. BAG-MEMBER( SOME-BAG-MEMBER(S), S)
INTU Physical bag or container, pieces of info. are stuffed inside/ pulled out with
no inspecition or interaction among them (including no check for multiple entries)
Provide intu. for each bag operation: member, insert, delete, equality.
TIES Up: Structure.
EXAMPLES {not} {bdy}
CONTENTS elements, including repetitions
STRUCTURE: Consider keeping the elements ordered s.t. ops. are more effic.
.SKIP TO COLUMN 1
⊗2SET⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick} class,collection, those...
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(ops, addl. ability, (recall all accepted transactions, poor, hist),
(recall order of insertion of present elements, good, list)
(number of deletions must at least equal no. of insertions before removal, good, bag)}
SPECIALIZATIONS
FILLIN: (defn, impose constraints (that each element must satisfy,,),
(that the collection of elements as a whole must satisfy(∃ele s.t.),,))
BOUNDARY {(operations, any addn/remov., (defn and intu, no longer same( (worth, lower)),
(contents, S ε S, (defn, no termination of recursion, (intu, zilch))),
(contents, S = {x | x≠S}, (defn, no termination, (formal thms, paradox)))}
WORTH (.8, .8, .7, .5, .4, .99, .9, (1.0 formal, .8 intu), .8, (1.0 basis))
INTEREST (some property exists tying the elements together besides membership, .9)
OPERATIONS {(membership: is x present or not?),
(some-member: access a member of the set),
(subset: test whether x is a subset of y),
(=: are two given sets equal: membership question always gives same ans.),
(insert: make x present as an element (until its next deletion)),
(delete: make an element x not present (until the next insertion))}
(not invariant: delete an element from a set which contains it)
(invariant: change the order of the elements of a list)
(invariant: insert any element into anyset which already contains it)
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(contents, altered, (delete any element or insert a new one))}
REPRESENTATION ((name of member)* not in any particular order)
VIEWS {(predicate over a universal set),
(operator, given some elements, make them into a set),
(bag or list where deletion means delete repeatedly until ele. is no longer a member)}
⊗5INFO GROUPING⊗*
DEFINITION Recall every element which has not been deleted since it was inserted.
A set is completely determined and specified by its members.
A member can be anything that already exists before starting to create the set;
after the set is created, elements which exist then can be inserted,
but the identity of the set produced then may change.
A set S is a list whose CAR is "CLASS".
CADR of the list structure is called an element of S.
When the CADR is deleted from S, the result W is called a tail of S.
Any tail of W is also called a tail of S.
Any element of W is also called an element of S.
The SET constraint is that no two elements may be equal.
Recursively: the list (CLASS) is a set, called the empty set PHI.
If S is a set, then so is (SET-INSERT e S), and e is called an element of S.
There are no other entities called sets; there are no other elements of S.
Two sets are equal, SET-EQUAL, iff either they are both PHI or else
one contains e as an element and the results of SET-DELETing e from each
structure are two new sets which are SET-EQUAL.
To insert an element e into a set S, call SET-INSERT(e, S).
To delete an element e from a set S, call SET-DELETE(e, S).
To test whether x is an element of S, call ELEMENT(e, S).
To access some element of a set, call SOME-MEMBER(S).
To test whether two sets S,R are equal, call SET-EQUAL(S, R).
To test whether S is a subset of R, call SUBSET(S, R).
(For readability, below, SET-EQUAL is abbreviated ==, its negation is ≠≠.)
∀x.∀y.∃1zε{T, F}. ELEMENT(x,y)={z}. So we abbreviate {T} as T below, etc.
For example, we could say: ∀x.∀y. ELEMENT(x,y) = T or ELEMENT(x,y) = F.
These relations satisfy the following conditions:
∀e.∀set S. ELEMENT(e, SET-INSERT(e, S)) = T
∀set S. ELEMENT(SOME-MEMBER(S), S) = (S≠≠PHI)
∀e.∀set S. ELEMENT(e, SET-DELETE(e, S)) = F
∀e.∀f≠e.∀set S. ELEMENT(e, SET-INSERT(f, S)) = ELEMENT(e, S)
∀e.∀f≠e.∀set S. ELEMENT(e, SET-DELETE(f, S)) = ELEMENT(e, S)
∀e. ELEMENT(e, PHI) = F
∀e.∀set S. ELEMENT(e, S) → S==SET-INSERT(e, S)
∀e.∀set S. ELEMENT(e, S) → S≠≠SET-DELETE(e, S)
∀sets S,R. S==R ↔ (∀e. ELEMENT(e, S) = ELEMENT(e, R)
∀set S. SUBSET(S,S) = T
∀sets R,S. SUBSET(R, S) = ∀e.(ELEMENT(e, R) → ELEMENT(e, S))
From the above, it follows e.g. that ∀set S, SUBSET(PHI, S)=T.
INTU List where eles. are people's names, hence same ele. name means same object.
Insertion involves first ensuring that it is not already a member.
Also: those pieces satisfying a certain proposition (no notion of order).
Also: Tagging elements from a universal set, with merely a yes/no tag.
Similarly: as a property: ask everybody yes/no question; the "set" is just those who say yes.
Similarly: as a pointer structure (a network of arrows)
Also: a square with points inside it. Also: a rectangle in the plane.
Intu. for ELEMENT, SET-INSERT, SET-DELETE should be tied to these preceding intus.
TIES Up: Structure. Ana: proof/truth/non-emptiness ←← perhaps discover this
EXAMPLES {not} {bdy}
CONTENTS elements
FILLIN: If building up, start from PHI. Add eles. in any order.
STRUCTURE: Consider actually keeping the elements ordered, and/or
duplicated, in such a way that the ops. are more effic.
.SKIP TO COLUMN 1
⊗2ASSERTION⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(justif, form, (complex but certain, good, theorem),
(not certain, fair, conjecture),
(known to be false, fair, counterexample),
(certain but assumed unjustifiable, good, axiom))}
BOUNDARY
WORTH (.6, .6, .9, .5, .6, .7, .6, (1.0 formal, .7 intu), .5, (1.0 basis))
INTEREST {(unintuitive, .9, psychology), (intutive, .5, satisfying)}
OPERATIONS {(substitute and see if it applies to this situation)}
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION predicate calculus representation is probably suitable here.
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION A statement of some existing relationship between some entities.
INTU Declaration of a relationship between pieces.
TIES Up: Object
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2AXIOM⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
WORTH
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION A true but non-justifiable statement.
INTU Declaration of a relationship between pieces so basic it cannot be analyzed.
TIES Up: Assertion
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Only with the explicit approval of the user. This is dangerous.
.SKIP TO COLUMN 1
⊗3ACTIVE⊗* Active Knowledge BEINGs; operations, relations, and properites.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
FILLIN: Extend the domain and/or range of the Active.
Special: new properties of enlarged dom and/or range, coincidences betw. them
SPECIALIZATIONS
WORTH: high
FILLIN: Consider coincidences between domain and range, simple pleasing relnships.
Constrain the domain and/or range of the Active.
Special: new props of enlarged dom and/or range, coincidences betw. them
Changing one of dom, range generally changes the other in an analogous way
In fact: the tying analogy can be thought of as the Active itself.
BOUNDARY {(intu, view as a static entity-- a subset of a X, (intu, wasted interp))}
DOMAIN/RANGE {not}
ORDERING(Complete)
WORTH (.5, .5, .5, .5, .6, .7, .6, (1.0 formal, .7 intu), .7, (1.0 basis))
INTEREST {(∃ other actives with same d/r, .5 + .5*(avg. int. of those other actives),),
(∃ other actives with similar d/r, .4 + .6*(avg. int. of other actives), poss. ana.),
(the active is of a known int. type (satisfies some int. prop), int. of that type,)
(the contents of β can be generated or checked in some way other than blind exhaustive
search through the definition, .3*ease of that way + .7* sqrt(int.))
Active A might be int. because Mapstruc(A, S) is int. for some strucs S; often
this is true because Mapstruc(A, S) will satisfy nice props. that S didn't.,.9)}
FILLIN: the above rules should be compiled at active-β-creation time.
OPERATIONS Includes properties that an Active β might satisfy. So big it gets a page.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
FILLIN: After one is known, the user may provide a pointer to an effic. sys. fn.
Often, infer recursive alg. from recursive definition.
Often, defined piecewise over the domain (a diff. alg. ∀ subset in a partition).
REPRESENTATION (Repr. as ⊂ X) or (Repr. as set of ordered pairs) or (Algorithm) or
(Repr. as set R of ordered pairs (x, S) where S={yεRange | xRy})
VIEWS {(⊂ X, set, (collection of elements, element = ordered pair),
(subset of a set, set = cross product: relation),
(subset of a set, no change: property)),
(pairs (x,S), active meta BEINGs, (do P resulting in one of these: Q,
activity P = operate with R on element x; set of outcomes Q = image set S)}
⊗5INFO GROUPING⊗*
DEFINITION A formal statement of an active connection shared by some entities.
One view might be that certain ordered pairs' eles. are all in the same relation;
another view would say that one can operate on any member of D in the same way;
Another view would say we are singling out those members of X sharing the same property.
One way to specify an Active β is: give its domain, its range, and
(for each element e of the domain) specify how to get β(e).
This last "how to" is typically an algorithm. β(e) means {xεRange(β) | (e,x)εβ}.
Along with each Active should be some indication of how to treat uncertainty;
often, the certainty of the result will be the minimum of the args' certainties.
INTU Some tie, some common statement true of the entities which are related.
TIES Up: Object, Specific Knowledge BEING. Down: operator, relation, property.
EXAMPLES {not} {bdy} Operation, Relation, Property ←← these are so nonspecific they may
be considered a sspecializations, not as examples.
FILLIN: Afterwards:
Huge interest but very temporary (unless quickly justified):
Make each new ex. into a new β, a new Active.
Note: this should cause the interesting parts of each new
example to be investigated (intu, exs, ties)
the defn. part of the new BEING is generally what is known immediately.
Apply each new Active α (viewed as an operator) to some domain eles,
and see if ∃ a good known reln. R (esp =) between that and some other
known reln r (esp. another composition).
That is, find interesting R,r such that R(r,α) holds.
Perhaps preface this by a quick query of r's and α's intuitions,
to see if they point to the relnship R.
Another interesting thing to look for is a known relation R such that
R(input, output) holds; that is, R=α on some restricted d/r.
WORTH: huge variation, but can be quite interesting.
CONTENTS
FILLIN: By pointing, explicitly, only if it seems to be small enough to do quickly.
Otherwise, stick with a symbolic characteriazation (defn, alg.)
.SKIP TO COLUMN 1
⊗2OPERATION⊗* A way to transform members from one concept into another.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(eles. of domain changed to some range eles., .90, .80, )}
FINAL {(Range ele., .60, .70, intu: final product of a manufacturing process)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(defn, augment, (reapply until no change, .75, find fixed point of the Op.))}
FILLIN: Increase its true domain, typically by modifying the definition.
Compute which known ops. tie parts of domain and domain to range; now
consider the class of all ops whose d/r satisfy precisely these constraints.
SPECIALIZATIONS {(domain of F is a cross-product, say AxB, .90, F called a binary operation.
Notation, in this case: c=F((a,b)) is written simply as c=F(a,b),
or even c=aFb. All these mean (a,b)Fc, i.e., that ((a,b),c)εF.
Repr/intu: 2-dimensional table, with entry c in row a, column b.
BOUNDARY {(intu, view as a passive entity-- a subset of a X, (view, relation)),
(extreme case: repeat op until no change is made or pattern of change is inferred),
(extreme case: for F:A→A, find xεA which is not in the image of A, x¬εF(A)),
(extreme case: result is no different than original argument, Op has no effect),
(extreme case: result is so different from original argument that intu is meaningless))}
DOMAIN/RANGE {not}
FILLIN: domain is some set D; range is some set R;
int. depends on D and R and properties which this particular operation possesses;
if high enough and no ptr, BEINGize this variant of the operation.
IF the op. can be viewed a subset of X, where X= AxBxCx...xZ, then
the domain can be any intial sequence of crossed sets A,B,C,.., and
the range is the remainder of those sets, crossed together.
ORDERING(Complete)
WORTH (.6, .6, .5, .4, .5, .6, .6, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST Int. property of result which is not true of arguments.
FILLIN: the interest rules should be compiled at op-creation time.
OPERATIONS Includes properties that an operation might satisfy, things one can do to it.
Apply.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
REPRESENTATION repr. as an Algorithm, or
Repr. as set R of ordered pairs (x, S) where S={yεRange | xRy}.
VIEWS to view as a reln: reln cross product is dom x range; (a,b)εR ↔ bεR(a).
to view as a prop: prop. master set is the whole dom x range; P((a,b)) ↔ bεP(a).
to view as a set: set of ordred pairs which is a subset of dom x range.
General view is that of a temporal sequence of actions (an alg.) to take to accomplish task R on x.
⊗5INFO GROUPING⊗*
DEFINITION A formal statement of an activity which can be performed on any element of a
specified type (the element must satisfy a certain property, belong to a
certain set called the domain). The results of such a transformation is to
produce one or more elements of (a subset of) another specified set (called
the range of the operation). One writes F(a)=B to indicate that B is the set of all
the results of operating with F on the element a. If B={b}, one might also
write F(a)=b, instead of F(a)={b}. One also writes aFb, (a,b)εF.
The operation F is more formally defined as the specific set of ordered pairs
(a,B) where aεdom and B⊂range, and F(a)=B, together with an explicit statement
of the domain and range of F.
The preimage of an element yεRange is defined as {xεdom | xRy}.
The image of an element xεdom is defined as {yεran | xRy}.
THe preimage of a given operation is defined as the preimage of the entire range,
meaning {xεdom | ∃yεran s.t. xRy}.
Similarly, the image of the op is the image of the entire domain, {yεran | ∃xεdom s.t. xRy}.
The system should discover facts relating these, like im(dom) = im(preim(ran)).
Viewing an operation as a temporal sequence, there must be some preconditions
true beforehand (this is related to the domain), and ther will be some statements
called post-conditions which will be guaranteed to hold afterwards (related to
properties of the range, and to the Final part of the specific op. Being
INTU Arrows emanating from intu. of one set's eles.; each arrow emanates from one
domain element, but has multiple heads which terminate in range elements.
The operation ⊗4is⊗* that set of arrows. Should notice that the set of all
arrow-connection therefore contains any operation as a subset.
TIES Up: Active Side: Relation, Property
EXAMPLES {not} {bdy} Insertion , Deletion, Convert-struc, Subst, Or, And, Not, Imply,
Unite, Common-parts, Setdifference, Compose
CONTENTS Since this is basically an activity, the alg. part is often the real "contents".
Sometimes: stored as if it were a relation.
.SKIP TO COLUMN 1
⊗2COMPOSITION⊗* Apply an operation to the result of a previous operation.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(eles. of dom. of 1st changed to some eles. of range of 2nd., .90, .80, )}
FINAL {(2nd range ele., .20, .70, intu: final product of a 2-step manufac. process)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Sequence of actions, an ordered pair of operations to perform.
FILLIN: Increase 1st true domain, typically by modifying the definition.
Increase 2nd range.
SPECIALIZATIONS Given an Active F:AxB→C, and an Active G:CxD→E, consider the new Active
h:(AxB)xD→E, written g*(fxi), defined as h((a,b),c)= g(f((a,b)),c). Alternatively,
given f:BxD→C and g:AxC→E, construct h:(AxB)xD→E as h((a,b),c)= g(a,f((b,c))).
An even further specialization: let some of A,B,C,D,E coincide.
An even further specialization: let all of A,B,C,D,E coincide.
BOUNDARY {(second operation doesn't care what the result of the first was, sequenceing unnec))}
DOMAIN/RANGE {not} (AOP↑2, OP, op)
FILLIN: domain is a pair of operations, range is a new operation whose domain
is the dom. of the 1st pair element, and whose range is the range of the 2nd.
int. depends on the 2 ops and on props which this particular op possesses;
if high enough and no ptr, BEINGize this new op.
ORDERING(Complete)
WORTH (.8, .95, .5, .5, .6, .9, .5, (1.0 formal, .8 intu), .8, (1.0 basis))
FILLIN: To forestall an infinite regress, decrease the activation energy of this investigation.
INTEREST Int. property of result which is not true of either argument relation.
Int. properties of both argument relations are preserved, undesirable ones lost.
Int. subsets (cases) of domain of 1st map into interesting subsets of range of 2nd.
Preimages of int subsets (cases) of range(2nd) are themselves interesting subsets of domain(1st).
The range of the first is equal to, not just a subset of, the domain of the second.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
FILLIN: Sequence: do 1st op (ALG), then take result and do 2nd op on it (ALG).
REPRESENTATION repr. as any operation, or perhaps just as 2nd o 1st.
VIEWS to view as a reln: view each arg. op. as a reln, R↓1 ⊂ AxB, R↓2 ⊂ BxC, composition
is a relation R↓2 o R↓1 ⊂ AxC, where (a,c) is in composition iff
(a,b) ε R↓1 and (b,c) ε R↓2.
to view as op: domain is dom of 1st, intermed. activity, then range is range of 2nd.
to view as a prop: prop. master set is (same notation) AxC; R↓2oR↓1(a,c)) ↔
R↓2(R↓1(a), c).
to view as a set: set of ordred pairs which is a subset of dom↓1 x range↓2.
⊗5INFO GROUPING⊗*
DEFINITION The sequencing of two operations, f and g, where domain of f contains the
range of g as a subset. E.g., f:A→D, and g:W→B with B⊂A.
Then the new combined operation is the composition of f and g, written
f o g, f(g), fg. The computation is straightforward; apply g and then apply
f to the result.
If f:AxB→C, g:D→A, and h:E→B, then one can consider the composition f o gxh,
also written f(g,h), whose value on (x,y) ε DxE is f(g(x),h(y)) ε C.
This is combinatorially explosive. Suggestions for containment: possibility of
considering f o gxg; f o ixj where at least one of i,j is the identity,
especially if the other one of i,j is equal to f itself; f o ixj, where one
of i,j is f, occasionally both are f. In general, f o gxh is about as intersting
as the ties between the three functions are already (equality is quite high).
To expand this flexibility, view any Active as an operation for these purposes.
The composition FoG is more formally defined as the specific set of ordered pairs
(a,B) where aεdom(G) and B⊂range(F), and B={F(c) | cεG(a)}, together with an
explicit statement of the domain and range of F and of G.
INTU Arrows emanate from one set, go into another set, new arrows go from there to
a third set. The composition means follow along and transfer to new arrows.
TIES Up: Operation
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2INSERTION⊗* Add new elements to a structure.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(a struc → larger struc, .60, .60, intu: direct)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(Dom/ran, restrict second argument to a certain type of struc,
(in AS, .90, set-insert),
(in AP, .80, INFIRST),
(in AP, .80, INLAST),
(in AB, .70, bag-insert)
(in AH, .40, hist-insert),
(in AL, .90, CONS))}
BOUNDARY {(args, equal, (defn/intu, paradox),(result automatically different)),
(2nd arg is the null structure, (result is poorly related semantically to first))}
DOMAIN/RANGE {not} { (AO x ASTRUC, ASTRUC←←not Null struc. ever,op),
(A0 x ASTRUC↑2, {T,F}, pred), (ASTRUC, AOxASTRUC, explosive operator) }
ORDERING(Complete)
WORTH (.7, .7, .7, .5, .5, .7, .3, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST When obj. is added, the struc. will be closer to having nice(r) properties.
Even though more stuff is stuck in, the nice(est) properties still hold, hence
they apply to the new elements (esp: the new ones don't intu. seem to satisfy them)
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: high. ⊗7should be easy to infer from axioms in definition⊗*
FILLIN: User provides a poiinter to very fast versions, but should still understand how.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Modify the given structure so that the given object is now inside it.
In some cases, this means doing nothing if it already is inside; in others,
it means adding it "again", keeping more than one "copy" of it as an element.tained in.
The following statements are true regardless of the type of structure:
Member(x, Insert(x,S))
∀x.∀y≠x.∀struc S. Member(x, S) = Member(x, Insert(y, S))
∀struc S. S≠Insert(S,S).
INTU Drop or push or tack on new piece or element into container or skeleton.
Potential exception: insert x into set or oset which already contains it: impermeable.
See the indiv. strucs for better intu.
TIES Up: Operation Side: Member, Delete
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2DELETION⊗* Removal of an element from a structure.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(a struc → smaller struc, .60, .60, intu: direct)}
FINAL {(given x is a member of a given struc, .70, .95, intu: direct from defn)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Domain, vastly extended, (reapply delete(x) to every
structural element of S, .65, delete x at all levels of S))}
SPECIALIZATIONS {(Dom/ran, restrict second argument to a certain type of struc,
(in AS, .90, set-insert),
(in AP, .80, INFIRST),
(in AP, .80, INLAST),
(in AB, .70, bag-insert)
(in AH, .40, hist-insert),
(in AL, .90, CONS))
((defn, augment, (reapply until no change, .65, delete all occurrences))}
BOUNDARY {(args, equal, (result, no change)),
(second arg, null structure, (result, automatically no change in it))}
DOMAIN/RANGE {not} { (AO x ASTRUC, ASTRUC, op),
(A0 x ASTRUC↑2, {T,F}, pred), (ASTRUC, AOxASTRUC, explosive operator) }
ORDERING(Complete)
WORTH (.5, .7, .7, .4, .5, .6, .2, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST When obj. is removed, the struc. will be closer to having nice(r) properties.
Even though stuff is janked out, the nice(est) properties still hold, hence
the removed material was not essential to giving S these properties
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: high. ⊗7should be easy to infer from axioms in definition⊗*
FILLIN: User provides a poiinter to very fast versions, but should still understand how.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Modify the given structure so that the given object is no longer inside it.
If it isn't inside to begin with, then there is no action to take.
The following statements are true regardless of the type of structure:
Member(x,S)) OR Not(Member(x, Delete(x, Insert(x, S))))←← it must discover this.
∀x.∀y≠x.∀struc S. Member(x, S) = Member(x, Delete(y, S))
∀struc S. S=Delete(S,S).
INTU Lift or pull out or break off a piece or element from a container or skeleton.
The resultant structure is very similar to the original structure, differing
only (at most) by the given object x.
Potential exception: Null structures. Try to pull x out of a structure not containing it.
See the indiv. strucs for better intu.
TIES Up: Operation Side: Member, Insert
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2CONVERT-STRUC⊗* View the type x structure as a type y structure.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(type of struc, .80, .80, intu: direct)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(Dom/ran, restrict each argument to a certain type of struc,,)}
BOUNDARY {(args, equal, (result, no change))}
DOMAIN/RANGE {not} { (TS = types of strucs x Strucs of 1st type, strucs of 2nd type,op),
(ASTRUC, TS x structures of the type specified by the element of TS, quasi-explosive op),
(TS x first types x second types, {T,F}, predicate)}
ORDERING(Complete)
WORTH (.6, .6, .6, .5, .5, .6, .7, (1.0 formal, .6 intu), .6, (1.0 basis))
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: high. ⊗7should be easy to infer from axioms in definition⊗*
FILLIN: User provides a pointer to very fast versions, but should still understand how.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Modify the given structure (its type is unknown, but accessable as CAR of its
representation), so it is now of type y; return the modified structure.
In some cases, this means doing nothing if it already is of type y.
In some other cases, the only change will be to the CAR of the representation.
In general, however:
Start with a given structure S. Ascertain its type, call that type x.
Ask y to create a new empty structure of type y.
Ask type x to give you the elements of S, one at a time; as each one
is reported, delete it from S and insert it into S'.
When S becomes an empty structure of type x, then the desired structure is S'.
INTU Redo everything the "right" way.
See the indiv. strucs for better intu.
TIES Up: Operation
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2SUBSTITUTE⊗* Replace one occurrence of x by y in S.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(a struc → similar struc, .60, .60, intu: direct),
(a struc containing x → sim. struc. that contains y where
it used to contain x, .80, .70, intu: direct)}
FINAL {(given y is in struc, no longer x, .70, .65, intu: direct from defn)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(Dom/ran, restrict second argument to a certain type of struc,
(in AS, .70, same as delete x; if x was in there, then insert y),
(in AP, .80, same as changing (x,←any≠x) into (y,$any), (nonx1,nonx2) unchanged,
and (nonx, x) into (nonx, y), and (x,x) into (y,y)).
(in AB, .70, same as pulling out x and sticking in y if x was found; notice how
the two ways of viewing deletion (all occurrences, 1 occurrence) are
here interepreted as substitute for all occurrences or just for 1.)
(in AL, .90, nontrivial interpretation. Must build up new list by peeling off
list eles. until x is found, then forget x and pretend you peeled y,
then put the old eles back from the newly created list.)
((defn, augment, (reapply until no change, .65, subst. for all occurrences))}
BOUNDARY {(first arg, of the form (x,x), (result, no change in second arg)),
(x is not in second arg, (result, no change in 2nd arg.))}
(second arg, null structure, (result, automatically no change in it)),
(second arg. is more of another type of β than a struc
(the argument list of an operator. This can be potentially more useful, though less "exciting"),
(a formal PC wff type of statement viewed as a struc, formally allowable if
y is free for x in the statement and we repeat until no change)),
(the two arguments are known to be equal or at least equivalent in this situation,
justification becomes formally acceptable)}
DOMAIN/RANGE {not} { (AP x ASTRUC, ASTRUC,op), (AP x ASTRUC↑2, {T,F}, pred),
(ASTRUC, AP x ASTRUC, explosive operator) }
ORDERING(Complete)
WORTH (.6, .6, .6, .5, .6, .6, .5, (1.0 formal, .7 intu), .7, (1.0 basis))
INTEREST When x is replaced by y, the struc. will be closer to having nice(r) properties.
x already is used nearby in a different context, and might be confusing.
Even though x is not there, the nice(est) properties still hold, hence
the precise identity of x was not essential to giving S these properties,
and the presence of y does not destroy them. Question: what about just deleting x?
Textual operation, replacing y by a functional equivalent, preserving truth.
Instantiation of a variable, to specialize a general proposition, for some purpose.
By doing this subst, we see that two very different things are equal. If the
subst. is legally allowed, we have proven something; if not, we jsut have an ana.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: high
FILLIN: User provides a poiinter to very fast versions, but should still understand how.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Modify the given structure so that the first element of the pair (x,y) is
is replaced by the second componenet of the pair.
If x isn't inside to begin with, then there is no action to take.
If there are more than one ocurrence, then only the first x is replaced.
The following statements are true regardless of the type of structure:
Member(x,S) ∨ ¬Member(y, Replace((x,y), S)
Member(x,S)) ∨ ¬(Member(x, Replace((x,y), Insert(x, S))))
Member(x, S) = Member(y, Replace((x,y), S)
∀z≠x,z≠y, Member(z, S) = Member(z, Replace((x,y), S).
INTU Magically transform the appearance of an x in some container so it now looks like a y.
The resultant structure is very similar to the original structure, differing
only (at most) in that there is one fewer x, and there is one extra y where x used to be.
See the indiv. strucs for better intu.
TIES Up: Operation Side: Member, Insert, Delete. Down: Assign
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2ASSIGN⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(where the variable x points to, .90, .85, intu: direct),
FINAL {(given var. x now points to entity y, .90, .95, intu: direct from defn)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Relax domain and range: substitute.
SPECIALIZATIONS {(Dom/ran, restrict second argument to a certain type of entity,)}
BOUNDARY Consider modifying the name of a variable as an assignment process.
DOMAIN/RANGE {not} { (AV x=(n,v) x any thing, modified x=(n,thing),op)}
ORDERING(Complete)
WORTH (.*, .*, .5, .5, .5, .6, .9, (1.0 formal, .6 intu), .6, (1.0 basis))
* means: if 'anyhting' is specified (in domain), then .5; else (in range) .0001 !!
INTEREST When x has the value y, some entity will be closer to having nice(r) properties.
Nice properties of something connected with x don't change when its value does.
Bad properties of x go away. A new thing is created simply by this change.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: high
FILLIN: User provides a pointer to very fast versions, but should still understand how.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Modify the given variable x so its value is now the entity y.
INTU Transform the place that x points to to y.
If y is in the domain, the caller is probably off his rocker!!
Given the value, choose the name; for example: naming a baby.
TIES Up: Substitute
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2MAPSTRUC⊗* Replace each member of a structure by the result of applying an Active to it.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(a struc with eles from dom(f)→ a struc with eles in ran(f), .60, .70, intu: direct),
(a struc containing x → sim. struc. that contains f(x) (or: an element of f(x))
where it used to contain x, .70, .70, intu: direct)}
FINAL {(op f is int.; see Active.Inteest for details, .40, .55, intu: I like you for what you
do to a group, not (just) what you do in private)}
PAST {(Trying to apply f to a structure, where it doesnt actually apply, but we know it ⊗4is⊗*
applicable to each individual element of the structure, .50, .60, teaching a class vs a human)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(Dom/ran, restrict the structure, (empty struc, .10, trivial; prob. mistake),
(singleton struc, .70, apply(some-member S))}
BOUNDARY {(struc is singleton, essentially the same as simply applying the op.)}
DOMAIN/RANGE {not} { (AOP x ASTRUC, ASTRUC of same type, op),
(AOP x ASTRUC↑2, {T,F}, pred), (ASTRUC, AOP x ASTRUC, explosive operator),
(ASTRUC x ASTRUC of same type, AOP, op: infer needed op by inverting/searching)}
ORDERING(Complete)
WORTH (.6, .6, .6, .5, .6, .6, .5, (1.0 formal, .7 intu), .7, (1.0 basis))
INTEREST When each ele z is replaced by f(z), the struc. will be closer to having nice(r) properties.
Even though eles have changed, the nice(est) properties still hold, hence
the op leaves these properties invariant on S (conjec: on all similar strucs)
Operation is itself v. interesting; or is EVAL; or is a predicate (so result is
just a structure of T's and F's, which ususally we apply CONVERT-TO-SET to).
By doing this mapping, we see that two very distinct strucs are related by f.
Sometimes we can prove that mapping a given op. will not alter the currently interesting
aspect of the structure (eg, doing row ops while int. in finding determinant of matrix).
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
FILLIN: User provides a pointer to very fast versions, but should still understand how.
REPRESENTATION
VIEWS Sequential (operate on one after another), Parallel (simult. group of workers).
View the struc. as one single entity, and instead of f consider the fn f' which
takes a struc as an arg and result.
⊗5INFO GROUPING⊗*
DEFINITION Modify the given structure so that each element is replaced by the result of
operating on that element with f. Alt: we may want to replace x by just one
element of (SOME-MEMBER of) f(x), especially if f is on AxA. In that case, f
will map a structure of elements of A onto a structure of elements of A.
Facts true about this should be constructable from axioms for Substitution and Struc. β's.
INTU Magically transform the appearance of each x in some container in the same way.
Interact with a group: you are really interacting with each individual member.
TIES Up: Operation Side: Subst, Apply. Down: Assign, Some-member
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2REVERSE ORDERED PAIR⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(order of the components, .95, .90, intu: switch)}
Invariant: Convert-to-set of the argument is precisely Convert-to-set of the result.
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY {(First and Last of pair are identical, result will be no change)}
DOMAIN/RANGE {not} { (APAIR, APAIR, op), (APAIR↑2, {T,F}, predicate) }
ORDERING(Complete)
WORTH (.7, .8, .6, .5, .4, .6, .8, (1.0 formal, .8 intu), .8, (1.0 basis))
INTEREST When reversed, some int. prop. will still be preserved.
OPERATIONS Mapstruc, Compose, Apply, Repeat ←← all these will be fairly interesting.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS Create new pair Q by Infirsting Last(P) into Q, and Inlasting First(P) into Q.
FILLIN: User supplies pointer to fast reverse.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION An ordered pair whose First is equal to the arg's Last, and whose Last
is equal to the old arg's First. Notice that the result will thus be the
same as the argument, if they are both viewed as Sets (eg, by Convert-to-set).
INTU Create new pair: see Alg. part.
Rearrange exsting pair: pull one out and move it over or move the remaining one over.
Shift perspective: walk around behind the structure and observe it from the rear.
TIES Up: Operation Side: Ordered Pair
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2RULE OF INFERENCE⊗* Combine true statements into new, true ones.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(true statements → diff, new true statements, .60, .80, intu: direct)}
FINAL {(true statement if args are, .70, .85, intu: direct from defn)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY {(justification, (exists, theorems about combining arguments))}
DOMAIN/RANGE {not} { (APR↑n, APR, op) }
ORDERING(Complete)
WORTH (.5, .3, .5, .5, .5, .6, .5, (formal: assumed, .6 intu), .3, (1.0 basis))
INTEREST Many interesting theorems are true iff we can assume this rule to hold validly.
The rule is intuitive.
OPERATIONS Apply; esp: substitutions
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS Apply this by matching args against templates, using substitution-matching.
WORTH: high
FILLIN: User provides a pointer to very fast versiions, but should still understand how.
REPRESENTATION (hyp,...,hyp,conclusion)
VIEWS Perhaps: as truth table operations.
⊗5INFO GROUPING⊗*
DEFINITION Operate on entities and preserve their truth. If the arguments, called the
⊗4hypotheses⊗*, are believed, then so must be the result, called the ⊗4conclusion⊗*.
INTU Laws, both political and physical. Constraints which must be obeyed.
Beaten paths, which are the only allowable routes through the jungle.
TIES Up: Operation, Side: Proof, Axiom
EXAMPLES {not} {bdy} Perhaps give it the following:
modus ponens, detachment, working forward
modus tolling, indirect proof, working backward
chaining, using previous proven results
subst. equivalent formulae
Subst definition of x in place of x
Subst x in place of its definition.
If y is known to be equal (equiv) to x, subst y for x.
Sometimes, only make the subst. for some of the x's in the current expression.
Make diff. parts look similar by selective substs. of this type.
specialization: from ∀x.P(x), we may conclude P(a). Here, both x and a are in a certain set.
From ∃x.P(x), if b ocurs nowhere else, we may conclude P(b(u,v,...,w)),
where u,v,w are all the universally-quantified variables preceding ∃x.
Special case: no such variables. Then conclude P(b).
generalization: from P(c), conclude ∃x.P(x). If c occurs nowhere else, conclude ∀x.P(x).
CONTENTS
.SKIP TO COLUMN 1
⊗2DISJUNCTION⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two statements → compound statement, .30, .60, intu: combine two ideas)}
FINAL
PAST {(no matter which of {a,b}, .90, .80, intu: recall only that one or both are wanted)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(Defn/intu, strengthen, (must not be both true, .3, exclusive or))}
BOUNDARY {(args, one is false, (contents, same as the other one)),
(args, one is true, (contents, must be true)),
(args, equal in contents, (contents, must be same as each of them))}
DOMAIN/RANGE {not} { (AP = any proposition, AP x AP,), (AP x AP, AP, op),
(AP↑3, {T,F}, pred), ({T,F}↑2, {T,F}, pred) }
ORDERING(Complete)
WORTH (.8, .7, .7, .5, .4, .7, .7, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST Know more about it than about any individual disjunct.
For example, P→A∨B is known to be true, but we are not sure about P→A or P→B.
Another case: interesting if the disjunction implies an interesting thing.
OPERATIONS Negate
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Change truth value of some of the arguments.
ALGORITHMS
WORTH: high. ⊗7should be easy to infer from definition⊗*
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given two statements, return F iff both are false; return T iff either is true.
Given a true statement, its disjoin will always be true.
Given a false statement, its disjoin with x will always be equal to the truth of x.
Given two equally true statements, their disjoin equals that truth value.
Given two just-probable beliefs, the disjunction is the maximun of the belief values.
The preceding line can be made to universally apply if true=1 and false=0.
INTU Pred: see if either of these will do.
View args.(and all statements) as sets, T/F = Nonnull/NIL. Then OR is just setunion.
⊗7Perhaps that last intuition gives away too much of the ana. betw. Logic and Set Thy.⊗*
TIES Up:Operation Down: Projection Side: Conjunction, Negation ←←perhaps
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2CONJUNCTION⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two statements → compound statement, .30, .60, intu: combine two ideas)}
FINAL
PAST {(both members of {a,b}, .90, .80, intu: recall only that both are wanted)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY {(args, one is T, (contents, same as the other one)),
(args, one is F, (contents, must be F)),
(args, equal in contents, (contents, must be same as each of them))}
DOMAIN/RANGE {not} { (AP = any proposition, AP x AP,), (AP x AP, AP, op),
(AP↑3, {T,F}, pred), ({T,F}↑2, {T,F}, pred) }
ORDERING(Complete)
WORTH (.8, .7, .7, .5, .4, .7, .7, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST The conjunction implies some interesting x which no single conjunct implies.
OPERATIONS Negate
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Change truth value of some of the arguments.
ALGORITHMS Pseudo-parallel satisfaction.
WORTH: high. ⊗7should be easy to infer from definition⊗*
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given two statements, return F iff either is F; return T iff both are T.
Given a false statement, its conjoin will always be false.
Given a true statement, its conjoin with x will always be equal to the truth of x.
Given two equally true statements, their conjoin equals that truth value.
Given two just-probable beliefs, the conjunction is the minimun of the belief values.
The preceding line can be made to universally apply if belief(true)=1 and belief(F)=0.
Given two desired goals, they are to (eventually) hold simulataneously.
INTU Pred: must ensure that all of these hold. Simultaneity, parallel, collateral.
View args.(and all statements) as sets, T/F = Nonnull/NIL. Then AND is just intersection.
⊗7Perhaps that last intuition gives away too much of the ana. betw. Logic and Set Thy.⊗*
TIES Up: Operation Down: Projection Side: Disjunction, Negation ←←perhaps
One meaning: simultaenous, parallel, no ordering constraint on args.
User may incorrectly mean: Sequence, ordered collection of entities.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2NEGATION⊗* This is a crucial process, which must be very knowledgable.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(anything → its opposite, .70, .60, intu: reverse everything)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Inequality
SPECIALIZATIONS
BOUNDARY {(when negation returns same value as started with, (intu, no change)),
(structures which have no clear opposite, (defn/intu, must collapse strucs. first)}
DOMAIN/RANGE {not} { (AP = any proposition, AP, operator),
(AP x AP, {T,F}, pred), ({T,F}, {T,F}, pred/op) }
ORDERING(Complete)
WORTH (.9, .8, .7, .5, .5, .6, .6, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST If the argument's truth value is extreme in either direction, then either it
or its negation will be a reliable, believed statement.
Interest is usually about te same as that of the argument.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Change truth value of the argument: negate itself.
ALGORITHMS
WORTH: very high.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION The statement whose truth is always the complement of the truth of the argument.
NOT(AND(x,y)) = OR(NOT(x),NOT(y))
NOT(OR(x,y)) = AND(NOT(x),NOT(y))
NOT(P with belief value v) = NOT(P) with belief value (1 - v) ←←opaque
NOT(∃x.P) = ∀x. NOT(P)
NOT(∀x.P) = ∃x. NOT(P)
NOT(T) = F
NOT(F) = T
NOT(NOT(P)) = P ⊗7Some or all of these should be proposed and proved, not supplied⊗*
INTU Op: this holds whenever the arg. fails, and fails whenever the arg. holds.
Flip, reverse, turn over, opposite, everything but, complement.
View args.(and all statements) as sets, T/F = Nonnull/NIL. Then NOT is just complement.
⊗7Perhaps that last intuition gives away too much of the ana. betw. Logic and Set Thy.⊗*
TIES Up:Operation, ≠. Side: And, Or ←←perhaps these shoudn't be explicitly provided.
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Reasonable always; doublecheck that doesn't already exist somewhere.
CHECK: Reapply NEGATION, should get back original argument. ←← perhaps opaque.
.SKIP TO COLUMN 1
⊗2IMPLICATION⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(reduce goal from x to y via pf. of y→x, .30, .60, intu: stepping stone)}
FINAL {(to prove x, prove y and y→x), .40, .50, intu: work on a good tool and how to use it)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS (certainty component, decreases, (some exceptions), (probable entailment))}
INTEREST: If you can weaken left side, with not much weakening of right side.
SPECIALIZATIONS
FILLIN: Adding some new conjunct to left side may add even stronger new change in right side.
BOUNDARY {(args, equivalent, (directionality of arrow is irrelevant)),
(args, truth value of one or both sides is known, (result is same as simpler expression))}
DOMAIN/RANGE {not} { (AP = any proposition, AP x AP,), (AP x AP, AP, op),
(AP↑3, {T,F}, pred), ({T,F}↑2, {T,F}, pred) }
ORDERING(Complete)
WORTH (.7, .8, .7, .5, .5, .7, .6, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST {(right side is one conjunct of left side, -.70, forgetfulness),
(left side is one disjunct of right side, -.70, grab onto coattails),
(short proof is known for this?, yes: -.30, no: +.70, (non)obviousness),
(right side is more int. than left side, .70+.30*(diff. in int.), improvement),
(right side looks harder than left side, .70+.30*(diff. in appearance), illusion)
(left side is known to be False, -.80, trivially (vacuously) true implication)
(left side is known True, .55, right side is actually a theorem)
(right side is known true, -.70, implication is trivially true)
(nothing much is known about the truth of either side, but we do know about the
truth of the implication, .90*(structural diff. betw. both sides), order out of chaos)
(both sides have some intu. connection (esp: entailment), .75, play a hunch)}
FILLIN: Add/subtract based on whether/how used it is over time.
OPERATIONS Negate; Prove: see Natural-Deduction.Algorithms.Hypothetical-World.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Change truth value of some of the arguments.
ALGORITHMS
WORTH: high. ⊗7should be easy to infer from definition⊗*
REPRESENTATION
VIEWS Perhaps give it some idea of truth tables; then supply table for Imply.
Perhaps give it info. on how to view this in terms of ∧,∨,¬.
⊗5INFO GROUPING⊗*
DEFINITION Given two statements, return T if both are T, if both are F, if the first
is F. Return F if the first is true and the second false.
A false statement may validly impy anything.
Anything may validly imply a true statement.
Anything implies itself (this follows from the above and bivalued logic)
The probability of belief(P→Q) is computed by viewing it as NOT(P)or Q.
Hence it is Maximum( 1-belief(P), belief(Q) ) which is necessarily ≥ belief(Q).
INTU Entailment, causality. Gating, permission, in-order-to.
Also added into this concept is the idea of vacuous reasoning.
The cases F→..., especially F→F, may be bizarre.
View args.(and all statements) as sets, T/F = Universal/NIL. Then IMPLY is just ⊃.
Exchange T/F interp. above, and IMPLY is like ⊂.
The satisfaction set of left hand proposition is ⊂ the satis. set of right one.
Positive reinforcement: A causes B which causes an even bigger A which causes...
TIES Up:Operation Down: And, Or, Not
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2UNITE⊗* Join two structures together.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two strucs into one struc, .80, .90, intu: join them together),
(new struc created, .40, .70, intu: when is the result diff. from either arg?),
(larger struc created, .50, .70, intu: ibid)}
FINAL {(existence of new large struc, .50, .70, intu: build on what you have already)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(dom/ran, restrict to particular type of structure,
(sets, .90, setunion or UNION),
(lists, .85, APPEND)
(bags, .70,)),
(dom, singleton struc, (access its element and then INSERT it, .80, INSERT))}
BOUNDARY
DOMAIN/RANGE {not} {(ASTRUC x ASTRUC, ASTRUC,),(ASTRUC, ASTRUC↑2,),
(ASTRUC↑3, {T,F}, pred)}
ORDERING(Complete)
WORTH (.7, .7, .6, .5, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST
WORTH: high ⊗7(this will get the system to fill this part in)⊗*
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: medium high
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given two strucs, produce one resultant struc, containing all eles. of each arg. struc
The relation is single-valued; its result will not have braces around it below.
Recursively: Unite(Null struc, x) = x = Unite(x, Null struc).
Unite(Insert(x,S), R) = Insert(x, Unite(S,R))
⊗7Possibly, the system should derive this recursive defn. for itself, from SET.DEFN and UNION.INTU.
In either case, this should easily lead via ana. to the SETUNION,APPEND functions.⊗*
Also: Unite(x,x) = x, etc.<See the list under COMMON-PARTS for what is really here>
INTU Push two strucs (as blobs) next to each other, then remove common boundary.
Ask each struc to dump its eles. into the new common one, one at a time.
⊗7Actually, there must be at least one of these for each way of intu. viewing the struc.⊗*
TIES Up:Operation Side: Common-part
EXAMPLES {not} {bdy}
WORTH: interesting.
CONTENTS
FILLIN: Reasonable to fill in iff contents of both args. are filled in.
.SKIP TO COLUMN 1
⊗2UNION⊗* Join two sets together.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two sets into one set, .80, .90, intu: smash them together),
(new set created, .40, .70, intu: when is the result diff. from either arg?),
(larger set created, .50, .70, intu: ibid)}
FINAL {(existence of new large set, .50, .70, intu: build on what you have already)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
DOMAIN/RANGE {not} {(AS = any set x AS, AS,),(AS, AS X AS,), (AS↑3, {T,F}, pred)}
ORDERING(Complete)
WORTH (.7, .7, .6, .5, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST
WORTH: high ⊗7(this will get the system to fill this part in)⊗*
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: medium high
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given two sets, produce one resultant set, its elements are those in any arg. set.
Recursively: Union(NIL, x) = x.
Union({e, C}, x) = {e, Union(C, x)}.
⊗7Possibly, the system should derive this recursive defn. for itself, from SET.DEFN and UNION.INTU.
In either case, this should easily lead via ana. to the APPEND function.⊗*
INTU Push two set blobs next to each other, then remove common boundary.
Ask each set to dump its eles. into the new common one; set rules will elim. duplic.
⊗7Actually, there must be at least one of these for each way of intu. viewing a set.⊗*
TIES Up: Unite Side: Intersection
EXAMPLES {not} {bdy}
WORTH: interesting.
CONTENTS
FILLIN: Reasonable to fill in iff contents of both args. are filled in.
.SKIP TO COLUMN 1
⊗2CROSS-PRODUCT⊗* Join two sets together into a set of ordered pairs.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two sets into one set, .70, .90, intu: position them together orthogonally),
(new set created, .40, .95, ),
(larger set created, .45, .80, intu: multiplication)}
FINAL {(existence of new large set, .40, .80, intu: build on what you have already)}
PAST {(want to compare each ele. of A to each ele. of B, .90, .98, intu: look at each pair)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (d/r, both args are themselves relations (say A:U→V, B:W→X; that is,
A⊂UxV and B⊂WxX), result is a new relation AxB from (UxV) to (WxX).)
BOUNDARY {(domain, one argument is too simple,
(null structure, result is null structure ←← it may discover this, so withhold it)}
DOMAIN/RANGE {not} {(AS = any set x AS, AS,),(AS, AS X AS,), (AS↑3, {T,F}, pred)}
ORDERING(Complete)
WORTH (.7, .7, .6, .5, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST Any ordered pair from these two specific sets will have some nice property,
often this is the property of being in the domain of a nice operation.
WORTH: high ⊗7(this will get the system to fill this part in)⊗*
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: medium high
FILLIN: should be fairly easy, using the defn. and MAPSTRUC β.
REPRESENTATION As a set, each of whose elements is an ordered pair.
VIEWS As the Universal relation with domain A and range B.
⊗5INFO GROUPING⊗*
DEFINITION Given two sets, produce one resultant set, its elements are ordered pairs,
(a,b), with aεA and bεB, and include all such ordered pairs.
That is, AxB = {(a,b) | aεA, bεB} = {(a,b)}↓[aεA,bεB].
Property: x is in AxB iff x is an ordered pair and First(x)εA and Last(x)εB.
Equivalently: (a,b)εAxB ↔ aεA ∧ bεB.
Procedurally: For each aεA, for each bεB, the ordered pair (a,b) is in AxB.
There are no other elements of AxB.
Recursively: NILxB = BxNIL = NIL. ←← prob. discovered by system.
{e}x{f} = {(e,f)}
{e, C}xB = {e}xB ∪ CxB
Bx{e, C} = Bx{e} ∪ BxC
⊗7Possibly, the system should derive this recursive defn. for itself, from SET.DEFN and CROSSPROD.INTU.⊗*
INTU Position 2 sets orthogonally, in different dimensions, considering each ele. as a cylinder.
All combinations of pairings; all possible marriages.
⊗7Actually, there must be at least one of these for each way of intu. viewing a set.⊗*
TIES Up: Unite Side: Ordered pair
EXAMPLES {not} {bdy}
WORTH: interesting.
CONTENTS
FILLIN: Reasonable to fill in iff contents of both args. are filled in.
.SKIP TO COLUMN 1
⊗2COMMON-PARTS⊗* Find each x which is substruc. of 2 given strucs.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two strucs into other strucs, .80, .90, intu: they must agree),
(new strucs created, .40, .90, intu: when is the result diff. from either arg?),
(smaller strucs created, .50, .90, intu: ibid)}
FINAL {(existence of new small struc, .50, .70, intu: seive with all the seives you have)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(d/r, restrict to one type of struc,
(sets, .90, intersection of the power sets),
(lists, .40, perform setintersection of the sets of sublists of each arg)
(bags, .40, perform setintersection of the sets of subbags of each arg))}
BOUNDARY
DOMAIN/RANGE {not} {(ASTRUC↑2,ASTRUC,op), (ASTRUC, ASTRUC↑2,), (ASTRUC↑3,{T,F}, pred)}
ORDERING(Complete)
WORTH (.7, .7, .6, .5, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST
OPERATIONS Maximize (it should probably discover this. This leads to setintersection).
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS Construct the set of all substructures of the first arg; then of the
second arg; then compute setintersection of these two sets; return this value.
Better: decide which arg is "smaller" structure, then move it along the
other arg, checking for substructure match. Perhaps view this as a search.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given two strucs, produce resultant strucs, each of which is
itself a substructure of ⊗4both⊗* argument structures.
Important note: this is not a function!
Therefore, below, CP(R,S) is still notated as a set of values.
General statements about the common part CP(R,S):
CP(Null struc, x) = {Null struc} = CP(x,Null struc)
CP(x,x) = set of all substructures of x
CP(x,y) = CP(y,x)
x is in CP(x,y) iff x is a substructure of y
x is never properly contained in CP(x,y).
CP(x, Insert(e,x)) = CP(x,x)
CP(x, Delete(e,x)) ⊂ CP(Delete(e,x)). Equality holds for unordered structures.
x and y are incomparable iff neither is in CP(x,y). ←← disc?
INTU Each substruc. of each of the two arg. strucs pushes itself up halfway; only
those in both get up all the way.
TIES Up:Operation Side: Unite
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Reasonable to fill in iff contents of both args. are small and filled in.
.SKIP TO COLUMN 1
⊗2INTERSECTION⊗* Find the common part of two given sets.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two sets into one set, .80, .90, intu: they must agree),
(new set created, .40, .70, intu: when is the result diff. from either arg?),
(smaller set created, .50, .70, intu: ibid)}
FINAL {(existence of new small set, .50, .70, intu: seive with al the seives you have)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
DOMAIN/RANGE {not} {(AS = any set x AS, AS,),(AS, AS X AS,), (AS↑3, {T,F}, pred)}
ORDERING(Complete)
WORTH (.7, .7, .6, .5, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST
WORTH: high ⊗7(this will get the system to fill this part in)⊗*
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: medium high
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given two sets, produce one resultant set, its elements are those in both sets.
Recursively: ⊗7{e} means (e, NIL). {e, C} means (e, C≠NIL).⊗*
∩(NIL, x) = NIL.
∩({e}, NIL) = NIL
∩({e}, {e, D}) = {e}
∩({e}, {f≠e, D}) = ∩({e}, D)
∩({e, C}, x) = Union( ∩({e}, x), ∩(C, x) )
⊗7Possibly, the system should derive this recursive defn. for itself, from SET.DEFN and INTERSECTION.INTU.
In either case, this should easily lead via ana. to List ∩-type functions.⊗*
INTU Each ele. of each of the two arg. sets pushes itself up halfway; only those in
the intersection get pushed up twice, hence are visible.
⊗7Actually, there must be at least one of these for each way of intu. viewing a set.⊗*
TIES Up: Common-parts Side: Union
EXAMPLES {not} {bdy}
WORTH: interesting.
CONTENTS
FILLIN: Reasonable to fill in iff contents of both args. are filled in.
.SKIP TO COLUMN 1
⊗2SETDIFFERENCE⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(two sets into one set, .40, .80, intu: second covers over first),
(new set created, .40, .70, intu: when is the result diff. from either arg?),
(smaller set created, .50, .70, intu: ibid)}
FINAL {(existence of new small set, .50, .70, intu: remove some parts of what you have)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
DOMAIN/RANGE {not} {(AS = any set x AS, AS,),(AS, AS X AS,), (AS↑3, {T,F}, pred)}
ORDERING(Complete)
WORTH (.7, .7, .6, .5, .5, .7, .8, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST
WORTH: high ⊗7(this will get the system to fill this part in)⊗*
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
WORTH: medium high
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given two sets, produce one resultant set, its elements are:
in the first set,
not in the second set,
all such elements.
Recursively: ⊗7{e} means {e, NIL}. {e, C} means {e, C≠NIL}.⊗*
-(NIL, x) = NIL.
-({e}, NIL) = {e}
-({e}, {e, D}) = NIL
-({e,D}, {e}) = D
-({e}, {f≠e, D}) = -({e}, D)
-({e, C}, x) = Union( -({e}, x), -(C, x) )
⊗7Possibly, the system should derive this recursive defn. for itself, from SET.DEFN and INTERSECTION.INTU.
In either case, this should easily lead via ana. to List-Diff. type functions.⊗*
Alternatively, we may say that -(x,y) is the complement of y relative to x.
If the first set is understodd, e.g. fixed in a given discussion, then we may
write -(x,y) as y', read y-complement; ' as an operator is also interesting.
INTU Each ele. of second set tries to pull its name out of first arg.
⊗7Actually, there must be at least one of these for each way of intu. viewing a set.⊗*
TIES Up:Operation Side: Union, Intersection Thms: lots of relnships involving ⊂,ε,=.
EXAMPLES {not} {bdy}
WORTH: interesting.
CONTENTS
FILLIN: Reasonable to fill in iff contents of both args. are filled in.
.SKIP TO COLUMN 1
⊗2PUT-IN-ORDER⊗* Arrange elements into some desired sequence.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(sequencing; next item to do/look at, .80, .80, intu: as a decider),
(Convert an unordered collection into an ordered one, .90, .80,)}
FINAL {(know what comes next, .70, .80, intu: as an operator)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(second argument, irrelevant, (minimize effort, convert-struc(x,LIST or OSET))}
(must be defined over entire cross-product, .85, linear order))}
BOUNDARY (First argument is structure which is already ordered by second argument, no change)
DOMAIN/RANGE {not} {(ASTRUC x AORDER, ALO = any list or oset,op),
(ASTRUC x AORDER x ASTRUC, {T,F}, pred),
(AORDER, ASTRUC↑2, explosive operation: use only for Examples purposes),
(ABAG x AORDER, ALIST, special op), (ASET x AORDER, AOSET, special op),
(ASTRUC↑2, AORDER, difficult operator; quasi-explosive) }
ORDERING(Complete)
WORTH (.5, .7, .5, .5, .5, .6, .5, (1.0 formal, .8 intu), .8, (1.0 basis))
INTEREST Some gain is produced when the elements of the given struc are in the given order.
Generally, this will be the order of later SOME-MEMBER accession; thus one
gain is that the order of fastest (qutomatic) peeling is the order of decreasing utility.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS The whole idea of an algorithm is to do things sequentially.
If the ordering is an algorithm which decides precedence, apply to all pairs
of elements of the structure and decide on the first element, then the next, etc.
Insert each at the rear; or insert at front and finally reverse; or find the
last element each time and insert at front each time.
One technique is to induce an order <↓S on the structure S, from another structure I,
called the index structure, where I is already ordered by <↓I.
We do this by finding an operation R:I→S which satisfies:
∀xεI. ∀y,zεR(x). y=z (that is, R must be single-valued),
and we now define our ordering <↓S as follows:
∀a,bεI, R(a) <↓S R(b) ↔ a <↓I b.
Notice that <↓S is total iff R is onto and <↓I is total when restricted
to some preimage of S.
REPRESENTATION <algorithm>; rarely specialized except to take advantage of special args.
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given a structure S, and an ordering relation <, create an ordered structure
S' whose elements coincide with those of S (they are equal under Conversion to Bags)
and for which <(a,b) implies that a precedes b in S' (for all a≠b ε S).
INTU The ordering are the directions for assembling the eles. of the struc, which are the pieces.
TIES Up: Operation, Obey orders Side: Ordering relation
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2RELATION⊗* A conection between an ordered pair of BEINGs.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(know whether given d/r pair is related in a given way, .80, .80,
intu: is the given pair a member of the relation?)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Relations Q s.t. R ⊂ Q ⊂ same cross-product that defines R;
Relations which are subsets of larger cross-products.
SPECIALIZATIONS Relations which are subsets of R; relations with slightly different
cross-products; those with similar cross-products and similar members.
BOUNDARY {(boundary of the cross-product of two sets)}
DOMAIN/RANGE {not}
ORDERING(Complete)
WORTH (.5, .5, .5, .5, .6, .7, .6, (1.0 formal, .7 intu), .7, (1.0 basis))
INTEREST
FILLIN: compile any interest factors at reln-creation time.
OPERATIONS Includes properties that a relation might satisfy. See esp. Active.Operations BEING.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(defn, satisfied, bdy. ops. of cross-product, subset)}
ALGORITHMS Walk through the entire cross-product and check for the reln.
REPRESENTATION (Repr. as ⊂ X) or (Repr. as set of ordered pairs)
VIEWS to view as an op: dom is first component of cross prod, range is second,
aFb iff (a,b) is in the relation F.
to view as a prop: prop. master set is the whole crossproduct, P((a,b)) ↔ (a,b)εP.
to view as a set: set of ordered pairs which is a subset of cross-product.
to view as a subset: subset of a cross-product.
⊗5INFO GROUPING⊗*
DEFINITION A formal statement of a property shared by some members of a cross-product.
For each such (a,b), we say it is in (a member of) R (this stresses that R is
a set). We might say aRb or R(a)=b to stress the fact that R can be viewed as
an op. Also R={(x,S) | xεdom and S={y | xRy}} and we say that S is the image of x.
This emphasises that it is an operator.
One can view R as {pεcross-prod. | (R p)} which emphasises that R is a property.
If R can hold between two equal entities, but in the current case the arguments
are unequal, then we say they are in ⊗4proper⊗*-R relationship, that "the R is proper" here.
INTEREST: Examine when R is proper and when it is not.
If, for x and y, either xRy or yRx, we say that x and y are ⊗4comparable⊗*.←← disc?
INTU Some tie, some common statement true of the pairs which are related.
Single-headed arrows emanating from intu. of one set's eles., terminating in another's.
The relation ⊗4is⊗* that set of arrows. Should notice that the set of all
arrow-connections therefore contains any relation as a subset.
2-dimensional lattice of elements of one set along each axis, with a dot at
coordinates (x,y) to indicate that the ordered pair (x,y) is in the relation.
2-dimensional table, with a mark in row x, column y to indicate (x,y)εR.
1-dimensional table, with entry y in slot x meaning (x,y)εR.
The above apply when R⊂AxB, and both A and B are manageably small sets.
If R' = AxB - R = {(x,y)εAxB | (x,y)¬εR} is much smaller than R, then store R'.
TIES Up: Object, Specific Knowledge BEING
EXAMPLES {not} {bdy} =, ε, ⊂, ≡, ≤, <, quantification
CONTENTS
FILLIN: Use algorithm if it is fast and if cross-product is small enough.
@2SPECIFIC RELATIONS⊗*
These actually fit in under RELN.EXAMPLES and RELN.SPECIALIZATIONS, as pointers,
so there will be no single "specific relations" BEING.
.SKIP TO COLUMN 1
⊗2EQUALITY⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(one entity into a diff-named one, .70, .80, intu: replace equal items)}
FINAL {(know whether x ∃, is just alias, .50, .70, intu: check for equality in known world)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (domain/range, both are of the same restricted type of β,
(both are sets, .90, set-equality),
(both are variables, .85, variable-equality),
(both are bags, .70, bag-equality),
(both are lists, .90, (list-)equality),
(both are hists, .40, hist-equality),
(both are pairs, .90, pair-equality))}
BOUNDARY {(Defn, weaken: equal only for given functions/known cases, (defn/intu,
absolute interchangability))}
DOMAIN/RANGE {not} {(AO = any objects, AO,explosive op), (AO x AO, {T,F}, pred)}
⊗7Actually, the arguments are names for objects, i.e., pointers, names of vars/β's.⊗*
ORDERING(Complete)
WORTH (.8, .9, .7, .5, .4, .8, .3, (1.0 formal, .8 intu), .7, (1.0 basis))
Actually: if domain is not AO↑2, then these weights drop very low (around .0001).
INTEREST The two entities originated in very different ways, hence nonintuitive.
Much is known about one of the entities (ties).
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
WORTH: High. ⊗7What changes do/don't destroy or produce an equality?⊗*
ALGORITHMS Syntatcticly identical.
Given 2 variables, see if they point to equal objects as their values.
Given one variable and one object, see if var points to that object.
Given one variable and one object, see if var points to an equal object.
Given two evaluable forms, evaluate each a variable number of times until results are equal.
Given 2 objects of type K, apply K-equal algorithms.
Given 2 objects, try to show that they are both of the restricted type K, for some K.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given an entity, find all other entities that it is identical to.
Given two entities, try to determine if there is any distinction between
what they encompass (find ele. of symm. diff. or else pf. of equality)
INTU Overlay two entities, see if there are any real differences.
By coincidence, two different formulations may specify the same thing.
Alias, AKA. Also: see intuitions for equivalence.
TIES Up: Relation Down: Equivalence, Subset/Implication ←←perhaps
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Reasonable to fill in when treated as a predicate, not as an op.
.SKIP TO COLUMN 1
⊗2MEMBERSHIP⊗* What structure(s) does a certain object belong to?
⊗5RECOGNITION GROUPING⊗*
CHANGES {(an element-name → name(s) of strucs, .80, .80, intu: as an operator)}
FINAL {(know if given ele. is in given struc, .90, .80, intu: as a predicate)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (dom/ran, restricted, (second AO replaced by AS, .90, set-membership),
(second AO replaced by AB, .70, bag-membership),
(second AO replaced by AL, .85, list-membership),
(second AO replaced by AP, .80, FIRST),
(second AO replaced by AP, .80, LAST),
(second AO replaced by AH, .80, hist-membership))}
BOUNDARY
DOMAIN/RANGE {not} {(AO = any objects, AO), (AO x AO, {T,F}, pred)}
ORDERING(Complete)
WORTH (.7, .8, .7, .5, .5, .7, .4, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST The struc was constructed in a very diff. way than postulating it contains this obj.
Int. ∀ thms. about struc (they could be used if can show obj. is an element)
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Add/delete eles. from the structure.
ALGORITHMS
WORTH: high. ⊗7should be easy to infer from recursive definition⊗*
REPRESENTATION
VIEWS {(predicate, containment, (predicate, first struc contains only first arg.)),
(op, containment, (op, first struc = struc containing only first object))}
⊗5INFO GROUPING⊗*
DEFINITION Given an object and a struc, see if the obj. is an element of the structure.
Given an object, try to determine what known and/or int. strucs it belongs to.
The following are true regardless of the nature of the structure:
For any structure and any object, membership is T xor it is F.
Recursively: Member(x, Insert(x S)).
Not(Member(x, Null Structure)).
∀x.∀y≠x.∀struc S. Member(x,S) ↔ Member(x, Insert(y, S))
INTU Pred: sift through struc elements, see if any is equal to the object to be tested.
Op: construct singleton containing obj; add eles. in various ways and watch for ∃/int.
Genl: each intu. repr. of each type of struc. should know how to test for membership.
TIES Up: Relation Side: Containment
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2CONTAINMENT⊗* What int/existing struct(s) is the given one a substruc of?
⊗5RECOGNITION GROUPING⊗*
CHANGES {(a struc → substructure, .60, .60, intu: step up to see a small part clearly)}
FINAL {(know if one given struc is part of another, .90, .75, intu: as a predicate)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS ∩
SPECIALIZATIONS {(Defn/intu, strengthen, (must not be equal, .5, proper containment),
(both args are to be viewed a particular type of structure; have special
properties to preserve depending on the type, .6,
subset: all elements of the first set are also elements of the second set
subbag: can remove an ele. of first bag from each bag until first is BNIL
sublist: first list is NIL or else CARs are equal and CDRs satisfy sublist
subpair: nothing here except pair-equality),
(both are ops, (suboperator: view op as a set, then just subset concept)),
(both args are (pointers to, names for) mathematical systems,
subsystem: cut out some members of the basis entirely, and/or replace a struc by
one of its substructures (and restrict all rele ops to this substruc), and/or
replace some operators by suboperators oo themselves))}
BOUNDARY {(args, equal, (intu, no larger)),
(contents, one ele of first is not in the second struc, (defn, not quite ∀))}
DOMAIN/RANGE {not} { (ASTRUC, ASTRUC, ), (ASTRUC x ASTRUC, {T,F}, pred) }
ORDERING(Complete)
WORTH (.7, .8, .7, .7, .6, .7, .3, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST Neither struc was constructed s.t. it is obvious that 2nd contains 1st.
Int. ∀ thms. about eles. of second struc (could use them if can show containment)
Int. thms. about second struc which say ∀ substruc...
Int. thms. about first struc which say ∀ superstruc...
Esp. if these thms. indicate results about the other arg. which are not obvious.
OPERATIONS Collect the set P↓S of all substructures of a structure S.
Conjecture which the system should notice or be told: S is determined uniquely by P(S).
also: the size of P↓S is always strictly larger than S.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS Sometimes(+): add eles. to 2nd struc; delete some from 1st struc.
Sometimes (-): Delete some ele. from 2nd struc; and/or add some ele. to 1st struc.
ALGORITHMS Perhaps give the system this operation: Power(S). This creates the structure
containing all substructures of S. If S is a set defined by property P,
then ∀R. R⊂S ↔ ∃property Q. R is defined by P∧Q; R ={x|P(x)∧Q(x)}={xεS | Q(x)}.
A subset A of S is created iff the defining property of A is the conjunction of
some property with that which defines S; equiv: property defining S is the disjunction
of the property defining A with some other property.
WORTH: high. ⊗7should be easy to infer from recursive definition⊗*
REPRESENTATION
VIEWS {(yes/no ∀ ele. of struc x, predicate (pred. over x,
satis. set = desired substruc viewed as a set)),
{(yes/no ∀ ele. of struc x, sequence of deletions from x,
elemets deleted = those who respond No)}
⊗5INFO GROUPING⊗*
DEFINITION Given two strucs, see if the first is a part of the second. See if each
element of the first is an element of the second, and if their order is preserved (somewhere).
Given a set, try to determine what known and/or int. sets it contains/ is contained in.
Recursively: ⊂⊂(Null struc, x) = T
⊂⊂(x, Null struc) ↔ x= Null struc
⊂⊂(Insert(y,Y), X) → Member(y, X) and ⊂⊂(Y, X)
The above implication is reversed for unordered structures; for
lists and osets and ordered pairs, the additional requirement is that
of all the places where CAR(Y) begins a role as substruc in X, the
(or "a") preceding element is y.
Universal: X ⊂⊂ Y iff ∀xεX (xεY) and any ordering on Y is preserved in X.
If, viewed as objects, one relation contains another, we say that R contains S,
S implies R, S⊂R, R⊃S.
INTU Pred: sift through set elements, see if any is equal to the object to be tested.
Construc. Op: construct singleton containing obj;
add eles. in various ways and watch for ∃/int.
TIES Up: Relation Down: Member. Side: Equality of strucs (⊂ and ⊃)
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Reasonable if second struc has known filled in reasonable-sized contents.
.SKIP TO COLUMN 1
⊗2EQUIVALENCE⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(reduce goal from x to y via pf. of y↔x, .30, .50, intu: just a new view)}
FINAL {(to prove x and y both, prove one and also prove y↔x),
.40, .50, intu: show same and then hope for one to work out)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS (specificity, decreases, (analogy), (similarity))}
SPECIALIZATIONS
BOUNDARY {(args, equal, (justif, is irrelevant)),
(args, truth value of one or both sides is known, (result is same as simpler expression))}
DOMAIN/RANGE {not} { (AP = any proposition, AP x AP,), (AP x AP, AP, op),
(AP↑3, {T,F}, pred), ({T,F}↑2, {T,F}, pred) }
ORDERING(Complete)
WORTH (.7, .8, .7, .5, .5, .7, .6, (1.0 formal, .8 intu), .7, (1.0 basis))
INTEREST {(one side is much easier to deal with in current context than the other,
but it is the hard side about which we must prove something)}
FILLIN: Add/subtract based on whether/how used it is over time.
OPERATIONS Negate
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Change truth value of some of the arguments.
ALGORITHMS Should be able to infer: demonstrate implication each way;
generalize this to showing that the arrows form a circle, for >2 simult. equivs.
WORTH: high. ⊗7should be easy to infer from definition⊗*
REPRESENTATION
VIEWS Perhaps give it some idea of truth tables; then supply table for Imply.
Perhaps give it info. on how to view this in terms of ∧,∨,¬.
⊗5INFO GROUPING⊗*
DEFINITION Equal for some current purpose, indistinguishable in some given respect,
interchangeable in some specified situation/usage.
Given two statements, return T iff their truth values agree.
Anything is equiv to itself (this follows from the above and bivalued logic)
The probability of P↔Q is computed by viewing it as P→Q and Q→P.
INTU Entailment, causality in both directions. Change your position and look again.
The cases F↔F, may be bizarre.
View args.(and all statements) as sets, T/F = Universal/NIL. Then EQUIV is just SET-EQUAL.
Resemblance, similarity, common features, uncommon statements true about both.
The current situ = room lighting; it is currently too dim to perceive any diff.
Functional indistinguishability (same specs, just different manufacturers).
TIES Up: Relation Down: And, Or, Not,Imply.
This concept might be discovered as an analogue of reversing-ordered-pair;
namely, when does Imply((a,b)) equal Imply((b,a)) ?
Perhaps this is too syntactic, but perhaps some nice intu. meshing exists.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2SCOPE⊗* Binding variables; analysis of bound vs. free.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(whether specific var has a meaning here, .60, .70, intu: constrain a var.)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Set, a subpart of all possible worlds.
SPECIALIZATIONS
BOUNDARY {(variable is unbound, free)}
DOMAIN/RANGE {not} {(Var-names x PR=any predicate/statement, {T,F}, pred),
(PR, list of var names, op)}
ORDERING(Complete)
WORTH (.5, .5, .4, .1, .7, .7, .5, (1.0 formal, .6 intu), .8, (1.0 basis))
INTEREST
OPERATIONS Can always widen; if x is not bound in y, can narrow: pull x out.
Substitution for a bound variable always means: replace every occurrence in its scope.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Quantification.
ALGORITHMS When you see <quantifier><variable>, or Define <variable>, then any old meaning
for the var. is forgotten, and the succeeding phrase, which defines the variable,
is acquired and held until further notice. The default lifetimes for such bindings are:
For math. theory entities: fixed throughout the theory, often eternally.
These include: basis strucs, basis actives, names for axioms, names for thms.
These variables should not be rebound during any pf, discussion of or
statement of any thm, ax, or basis entity.
For variables and symbols introduced or bound during a proof or a single statement:
fixed throughout that proof/statement; often, continues until next rebinding.
If the binding occurs between proofs, as a definition, it may hold throughout the
remainder of the theory. If it occurs earlier, this probability decreases.
REPRESENTATION typically, just the fact that a certain entity, ususally a variable x,
is constrained in some way (to take on a certain value, to take on only values
from a certain set) for a while (usually, in the following statement or paragraph).
Syntactically, one might say ...x such that P(x)...., which binds x to the
set defined by P, for the duration of this statement. Or, let x... constrains
x, often for a whole paragraph. Define x... is a permanent constraint.
VIEWS {(the statement(s) over which a quantified variable is constrained)}
⊗5INFO GROUPING⊗*
DEFINITION When a variable is quantified, its scope is the statement(s) which follow
the quantification form immediately in the next form. Any usage of that variable
nme in that form is called ⊗4bound⊗*, and any variable which is not bound is
called ⊗4free⊗*. Legally, one may substitute x for y in some form z iff
no pre-existing free occurrence of y now becomes a bound occurrence.
Another way this phrase might be used is in any type of constraint, where it
applies only in certain cases or for a certain time; such constraints help
delimit the scope of the constraint (where it holds power automatically).
INTU The kingdom over which the constrain wields power; the limits of his authority.
A prison, in which a variable is confined for a fixed term, in fixed ways for
some reson.
TIES Up: Relation, Quantification
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2QUANTIFICATION⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(2nd becomes more definite, .60, .70, intu: constrain a var.),
(1st acquires a new meaning, .45, .55, intu: overwrite a cell in memory)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS A few known types of quantification: ∀,∃,etc.
BOUNDARY {(1st arg does not occur in 2nd, (result, no change))}
DOMAIN/RANGE {not} {(AV x PR=any predicate/statement, PR)}
ORDERING(Complete)
WORTH (.5, .5, .4, .1, .7, .7, .5, (1.0 formal, .6 intu), .8, (1.0 basis))
INTEREST {(The result is a statement which is quite surprising, or whose corrol is)}
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS (the result is just (name-of-quantifier first-arg-name)(second arg))
REPRESENTATION ((<quantifier> <1st> in <set>) <2nd>). in-set may be replaced by
a condition, (<quan><1st> such that <condition on 1st>, <2nd>).
VIEWS {(constrains the first arg name to mean something specific in the second arg)}
{(second arg is true in some cases, name of quantifier helps explain which sits)}
⊗5INFO GROUPING⊗*
DEFINITION A formal statement of which elements a property is known to hold for.
The set of possible eles. is mentioned or implied, and a name given to a
representative member of that set which satisfies the given constraint.
In (quan 1st in set)(2nd), the statement "2nd" is stated to be true when the
variable "1st" (which may or may not occur inside 2nd) is "quan"-member of
the given set (quan will become either "some" or "any" or "precisely one",etc.)
For each such 1st, we say that it satisfies 2nd. Viewing 1st as a variable,
we say that its domain of values is <set>, that <set> is the set of its poss. values.
Thus quantification is an odd sort of realtion; perhaps it is a meta-concept.
INTU 2nd is true in some cases, depending on how certain variable slots are filled
in. The quantification constrains the satisfiable values of a single variable.
TIES Up: Relation Side: Theorem
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2UNIVERSAL QUANTIFICATION⊗* For all "var" in "set", "statement" holds.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(2nd becomes more definite, .55, .70, intu: constrain a var.)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY {(almost always, empirically always, set is null → vacously true}
DOMAIN/RANGE {not} {(AV x PR=any predicate/statement, PR)}
ORDERING(Complete)
WORTH (.6, .6, .4, .05, .7, .7, .4, (1.0 formal, .6 intu), .8, (1.0 basis))
INTEREST {(2nd seems to hold only for some, not for all, elements of the given set)}
OPERATIONS Specialize: replace var by any known member of the set.
Negate.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Consider only the subset of the set where 2nd ⊗4does⊗* hold.
Disjoin to 2nd the special exceptions which can occur(all eles. of set not satisfying 2nd)
(-): add to set some element not satisfying 2nd.
ALGORITHMS
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION The object x which may occur in 2nd can be replaced by any member of
an auxilliary-memtioned set, and 2nd will still be true.
One may say that the set ⊗4satisfies⊗* the 2nd.
INTU 2nd is true in all cases, when x is replaced by any specific member of the given set.
TIES Up: Quantification Side: Prove, Theorem
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2EXISTENTIAL QUANTIFICATION⊗* There exists...
⊗5RECOGNITION GROUPING⊗*
CHANGES {(2nd becomes more definite, .55, .70, intu: constrain a var.)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS ∃1 ←← this should be discovered along with the idea of Singleton set.
BOUNDARY {never, ∃1, almost always,∀}
DOMAIN/RANGE {not} {(AV x PR=any predicate/statement, PR)}
ORDERING(Complete)
WORTH (.6, .6, .4, .5, .7, .7, .4, (1.0 formal, .6 intu), .8, (1.0 basis))
INTEREST {(2nd seems never to hold on elements of the given set)}
OPERATIONS Specialize: consider var a specific (but unknown) member of the set.
Negate.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} (find an x somewhere satisfying 2nd, then insert it into 2nd)
ALGORITHMS
REPRESENTATION
VIEWS In the present world, we can find such an entity. Note that the current world
may be hypothetical, for example if there were previous quantifiers which
said ∀q or ∃q,... then we may assume that we have q in hand and it exists.
⊗5INFO GROUPING⊗*
DEFINITION The object x which may occur in 2nd can be replaced by some member of
an auxilliary-memtioned set, and 2nd will be true (the acutal name may be unknown).
One says that 2nd is ⊗4satisfiable⊗* in the set.
INTU 2nd is true in some cases, when x is replaced by a specific member of the given set.
TIES Up: Quantification Side: Prove, Theorem
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2UNIVERSALLY NEGATIVE QUANTIFICATION⊗* Never... For no...
⊗5RECOGNITION GROUPING⊗*
CHANGES {(2nd becomes more definite, .55, .70, intu: constrain a var.)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY {never, ∃1, almost always,∀}
DOMAIN/RANGE {not} {(AV x PR, PR)}
ORDERING(Complete)
WORTH (.5, .6, .4, .05, .7, .7, .4, (1.0 formal, .5 intu), .6, (1.0 basis))
INTEREST
OPERATIONS Negate.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION The object x which may occur in 2nd can be replaced by any member of
an auxilliary-memtioned set, and 2nd will be false.
One says that the 2nd is ⊗4unsatisfiable⊗* in this set.
INTU 2nd is false in all cases, when x is replaced by a specific member of the given set.
TIES Up: Quantification Side: Prove, Theorem Equiv: Not(∃).
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2EXISTENTIALLY NEGATIVE QUANTIFICATION⊗* Not for all... For some x, not...
⊗5RECOGNITION GROUPING⊗*
CHANGES {(2nd becomes more definite, .55, .70, intu: constrain a var.)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY other quantifiers
DOMAIN/RANGE {not} {(AV x PR, PR)}
ORDERING(Complete)
WORTH (.5, .6, .4, .5, .7, .7, .4, (1.0 formal, .5 intu), .6, (1.0 basis))
INTEREST
OPERATIONS Negate.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION The object x which may occur in 2nd can be replaced by some member of
an auxilliary-memtioned set, for which the 2nd will be false.
One might say that the set does not ⊗4satisfy⊗* 2nd.
INTU 2nd is false in some cases, when x is replaced by a specific member of the given set.
TIES Up: Quantification Side: Prove, Theorem Equiv: Not(∀).
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2NEITHER NEVER NOR ALWAYS⊗* For some, but not for all...
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY other quantifiers
DOMAIN/RANGE {not} {(AV x PR, PR)}
ORDERING(Complete)
WORTH (.5, .6, .4, .5, .7, .7, .4, (1.0 formal, .5 intu), .6, (1.0 basis))
INTEREST
OPERATIONS Negate: [low interest result (for all or for none); exclusive extreme]
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION The object x which may occur in 2nd can be replaced by some member of
an auxilliary-memtioned set, for which the 2nd will be false, and by some other
member for which it will be true.
INTU There are cases known in which 2nd is false, some for sure where it is true.
Sets: A non-null proper subset.
TIES Up: Quantification Side: Prove, Theorem.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2PROPERTY⊗* A predicate, a condition which an entity might satisfy or not.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(ability to know whether a given β in family F satisfies a certain criteria, .80, .85,
intu: view as an operation with one argument, over domain F, which returns T or F),
(know what theorems can be used rele. to β, .30, .60, intu: find out β's type)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(domain, constrain to be in a certain form,
(set of all relations, .90, reln.operations),
(a cross-product X, .90, a relation))}
WORTH: high
BOUNDARY {(domain is some specific set of elements, thus this concept is = subset),
(range is a singleton subset of {T,F}, then this (or its negation) is a theorem)}
DOMAIN/RANGE {not} {(any set, {T, F}, op), (any set, all its elements which satisfy P, passive)}
ORDERING(Complete)
WORTH (.6, .7, .5, .5, .6, .8, .7, (1.0 formal, .6 intu), .6, (1.0 basis))
INTEREST {(interesting as a subset or as a reln or op, that level of int., direct),
(new theorems about BEINGs which satisfy this proposed property,
.6 + .4*(avg. int. of thms.), coincidences are rare and wondrous),
Also: (how neatly the family F breaks into T/F classes,
(along subfamily lines, +.95),
(within single specific β's ε F, -.85),
(not all T nor all F, else this is just a theorem (its negation is a thm)))}
OPERATIONS Property itself; Relns.Operations; Set.Operations.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS Must be able to check each member of F and decide whether T or F.
REPRESENTATION
VIEWS as a relation: cross-product of domain set and range {T,F}; (a,b)εR ↔ R((a,b))={T}.
as an operation: domain is domain set, range is {T,F}, no doubleheaded arrows.
aFb ↔ F((a,b))={T}.
as a set (as a subset): {xεdomain | P(x)={T} } = PSET. Thus P(x)={T} ↔ xεPSET.
⊗5INFO GROUPING⊗*
DEFINITION An operation whose range is {T,F}. Since we only distinguish the case when
R(a)={T} from all others ({F}, {}, {T,F}) we may as well assume that the ⊗4only⊗*
possible values for any x in the domain are {T} and {F}.
PSET, all its subsets, and all its elements are said to ⊗4satisfy⊗* the property P.
For each entity B satisfying the predicate P, we say that B is P (P adjective)
or B has property P, or that P(B) holds, or that B is of type P.
FILLIN: If a good intuition exists for the property Q: Consider the set PP(S)={A | A⊂SxS}
where S is a set whose elements are likely to be in the domain of relations which
which meaningfully satisfy or fail Q. Notice that PP(S) is also the set of all relations
on SxS. Locate those members x of PP(S) which intuitively satisfy the desired property Q.
Now try to find some common properties, some conditions all these x's share.
Perhaps go back and select a new S (repeat this a few times).
Weed out those which are not certain and/or which can be derived from (or which
contradict) the others. Those which remain are conjoined into the definition of Q.
Notice that this works only for properties Q which can be easily built out of
already-existing Actives. This should not be a practical or a theoretical restriction.
INTU Some tie, some common statement true of the domain eles. which have this property.
Similarities in details of the arrows which connect sets; a ⊗4type⊗* of arrow.
TIES Up: Active, Operations Archetypical BEING.
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Use algorithm if it is fast and if domain is small enough.
Use thm: any reln. having prop. A, B,... must also have ⊗4this⊗* property.
.SKIP TO COLUMN 1
⊗2ORDERED⊗* Are a structure's elements in proper precedence sequence?
⊗5RECOGNITION GROUPING⊗*
CHANGES {(sequencing; next item to do/look at, .85, .85, intu: as a decider),
(Convert an unordered collection into an ordered one, .85, .85,)}
FINAL {(know what comes next, .85, .80, intu: as an operator)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(dom/ran, restricted, (each is the pair {x,y}, .95, ordered-pair),
(each is the set S, .50, oset),
(each is the bag B, .90, list)
(each is the bag (BAG a b), .95, ordered pair (PAIR a b) or (PAIR b a))),
(do not contain (x,y) or (y,x) for all x and y in the structure, .60, partial ordering))}
BOUNDARY (order of eles. in one pair in <, irrelevant, partail order is okay)
DOMAIN/RANGE {not} {(bag or set S,itself, op), (S x itself, {T,F}, pred),
(AB, AL, put a bag in order: op), (AS, AOSET, put a set in order: op)}
ORDERING(Complete)
WORTH (.6, .7, .7, .6, .6, .7, .4, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST Some gain is produced when considering the elements in the given order.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS The whole idea of an algorithm is to do things sequentially.
REPRESENTATION (preceder, succeeder, Can/Must/Mustnot/Might)* or <Algorithm>
VIEWS Sequence of things; esp: sequence of operations to perform.
Sequence of things in an ordered structure; the order they are removed in.
⊗5INFO GROUPING⊗*
DEFINITION Superiority, in a given respect, in the current aspect of comparison.
Given a bag or set, called S, constrain its elements by a relation < s.t.
∀a,b,cεS. <(a,b) ∧ <(b,c) → <(a,c)
Strong: ∀a,bεS. <(a,b) → NOT(<(b,a))
or Weak: ∀a,bεS. <(a,b) ∧ <(b,a) ↔ a=b
Alternate axiom for Strong: ∀aεS.¬<(a,a).
Sometimes, add this Strong LINEAR ordering axiom: ∀a≠bεS. <(a,b) ∨ <(b,a)
For Weak Linear ordering, omit the "≠b" in the above axiom.
Sometimes, even add this Strong WELL ordering axiom: ∀B≠PHI ⊂ S, ∃xεB. ∀y≠xεB. <(x,y).
Alternate statment of this axiom: Each nonempty subset of S has a least element.
For Weak Well ordering, omit the "≠x" in the above axiom.
Including LINEAR, one can arrive at the idea of a unique successor, SUCC(x).
and also the idea of a first element, one which is < all others.
Each oset and each list implicitly specify a unique LINEAR order relation:
The cells which hold the information in a list are in order; accessing the
front element means accessing that element which is < every other.
For osets, the order is easier since there are no repeated elements.
Notice that any subset of an ordering relation is also an ordering relation;
this does not necessarily apply to LINEAR ordering relations (also called TOTAL).
Nonlinear ordering relations are also called PARTIAL orderings.
INTU Can only do one thing at a time; do x before y if <(x,y).
Specialization: "doing a thing" →→→ "occupy a certain cell in ordered structure".
Operator: what can be done after this one but not before it? Which must be done before?
Temporal sequence. Order in an ordered structure. Sequence of operations to do.
Advancing a state variable, incrementing a counter, going to the next one.
Following a causal arrow; the ironclad precedence of the cause before the effect.
Preconditions; factors which enable another entity; the result of x is needed before
we can even start to do y; compose operations. If the ordering is not total,
if sometimes it doesn't matter what we do, then the ordering is only ⊗4partial⊗*.
Superiority, to the left of, earlier, above, younger than, ancestor to.
Specialization of this: do → occupy cell in a list or oset or ordered pair.
Op: what elements should be done after this, not before?
Antonym: parallel, simulataneous. This includes one of the two meanings of AND.
TIES Up: Property, Relation Side: Ordered pair, List, Oset
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2CLOSURE⊗* Generate a substructure from a core, using an operation.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(op f will now no longer take you out of (slight enlargement of) core,
.90, .80, intu: make just enough room to live in)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(dom/ran of op f, both are equal to A which is a subset of S, .85,
so closure is just A ∪ f(A) ∪ f(f(A)) ∪ ...,
which is of course a subset of S and a superset of A),
(the set A is a singleton {a}, .80, )}
BOUNDARY {(dom (args), extreme, (A is null, .40, A is vacuously closed under any op f),
(f is the empty relation, .10, every A is vacuously closed under f),
(f:S↑n→S but f has no preimage on A↑n; that is, ∀x↓1,...,x↓nεA, f(x↓1,...,x↓n)=PHI.))}
DOMAIN/RANGE {not} {(Astructure↑2 x AOP, Astructure,op),
(ASTRUC↑3 x AOP, {T,F}, pred), (ASTRUC x AOP, ASTRUC↑2, explosive op)}
The second structure A must be a substructure of the first one S. The operation
.ONCE TURN ON "[]"
f must be from S↑n to S (i.e., viewed as a relation, f ⊂ A↑[n+1]).
The final structure will also be a substructure of S.
ORDERING(Complete)
WORTH (.6, .6, .4, .6, .6, .6, .6, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST The operation f can be restricted to closure(A)↑n to itself instead of S↑n to itself.
Thus the newly restricted operation will probably satisfy the same properties
on closure(A) as f did on S. Check for these. The biggest advantage is that
one can take elements from cl(A), operate on them with f, and get new elements of cl(A))
One interesting thing to look at is cl({z}); another is which subsets satisfy
the equality X=cl(X); another is the conjunction of these two: which zεS satisfy
closure({z}) = {z}. Any such z are called fixed points of f.
OPERATIONS Interesting to look at closure(closure(A)).
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS The obvious alg: set C←A. Compute f over C↑n, and add in any nee eles of S.
Repeat until there are no new additions, that is, until f(C)⊂C.
REPRESENTATION
VIEWS A property that some substructures possess.
An operation that can be performed on any substructure.
A repeated composition of f with itself, arbitrarily deeply.
⊗5INFO GROUPING⊗*
DEFINITION Given a structure S and an operation f:S↑n→S, we shall say that a substructure
A of S is ⊗4closed⊗* under f if f(A↑n)⊂A. The ⊗4closure⊗* of a substructure A
of S is the smallest closed substructure of S which contains A; this is written
cl(A); alternative definition: the intersection of all closed substrucs of S
which contain A; the union A ∪ f(A↑n) ∪ f(f(A↑n)↑n) ∪...; the previous union,
stopped as soon as the new set unioned in is already contained in the union.
Notice that f(A↑n) means {xεS | ∃z↓1,...z↓nεA s.t. f(z↓1,...,z↓n)=x}.
Notice that A ≤ cl(A) ≤ S, where "≤" means the relation substructure (containment).
INTUITION Keep adding new friends to your group until nobody knows anybody else to add.
Repeatedly apply a function to what is known until it no longer gives any new info.
Progress linearly, nondeterministically; if you ever repeat a state, you may as well stop.
TIES Up: Property, Operation. Side: Composition
EXAMPLES {not} {bdy} (+): For any S and f, S is closed and PHI is vacuously closed.
The closure of any substructure is closed and is in fact its own closure.
CONTENTS
.SKIP TO COLUMN 1
⊗2EXTREME⊗* Within a given example of a β, what are the subconcepts specifying its extremities.
Possibly, this β should actually be Archetypical: should be made into a part name.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(there is nothing more in this direction, .80, .75, intu: go till you hit a wall)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(extremes of a concept are its boundary, qv, .80, Boundary and Bdy-exs parts),
(extremes of an instance of a concept are subpart(s) which are distinguished
by universal statements proclaiming their sup(inf)eriority wrt some specific measure;
often this measure is (satisifes the defn of) an ordering on the instance.
An extreme should be generally meaningful for any instance of this concept)}
BOUNDARY (instances are other β's, then this is indistinguishable from the Boundary part)
DOMAIN/RANGE {not} {(an instance of a β, an extreme subpart of that instance, an op),
(any β, a property which takes an instance of β and produces its extreme subparts, op),
(any entity x any subpart of that entity, {T,F}, predicate)}
ORDERING(Complete)
WORTH (.6, .6, .5, .4, .6, .7, .4, (1.0 formal, .7 intu), .8, (1.0 basis))
INTEREST The extreme subpart(s) satisfy int. props that just any old subpart might not.
OPERATIONS An interesting thing happens if we try to compose this concept with itself;
the results are all interesting (the upper bounds to the set of all upper bounds
in B of a set A are just the Greatest elements of B;
the Least of the set of upper bounds is lub, a very important concept; etc.).
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS To test whether x is the extreme part of S, consider going to x from
various other subparts of S, then try and keep going in the same way; if you
can, then what you get is "more extreme" than x. If you can show that you can
always continue in that direction, then there is no extreme subpart in that direction.
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Given a comparison function, say f:AxA→{T,F} (or, equivalently, f⊂AxA),
two extreme classes of elements of A, in the direction of f, are:
maximum↓f(A) = {xεA | ∀y≠xεA. f(x,y)}, and
minimum↓f(A) = {xεA | ∀y≠xεA. ¬f(x,y)}.
For ordered structures, this will become the notions of First and No-Successor.
For totally ordered structures, these are First and Last.
When A is still thought of as a set, we call these concepts Greatest and Least.
A relaxation is specify that the extremes lie only in some set containing A:
Given A, B, f⊂BxB, then a Lower bound of A is any xεB s.t. ∀y≠xεA. f(x,y).
Similarly, an Upper bound of A is any xεB s.t. ∀y≠xεA. ¬f(x,y).
Another dimension, given our f as above, is to compose f with itself until
there is no change in the resultant subset of A produced, or until the pattern
of the change is inferred and actually guessed at as a conjecture.
The other extreme, again given our f⊂AxA, is to consider {xεA | x¬ε f(A)},
the set of elements which have no preimages under f.
Another tack to take is to consider the fixed points, {xεA | x f x}.
A stronger extreme this way, if the former set is too big, is {xεA | f(x)={x} }.
Finally, one can look for those elements which go nowhere under f⊂AxB, namely
{xεA | f(x) = PHI } = preimage of NIL = those elements which have no image.
INTU The farthest one can go; walk till you are constrained by a wall (the defn, eg).
TIES Up: Property Side: Ordered, Statement of Generality
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2ACTIVE.OPERATIONS⊗* Properties, e.g. inverse, compose, repeat, function,...
Should be independently discovered by the system, not supplied by the creators.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(know whether given Active(s) satisfy certain property, .70, .80,
intu: operation is a (n-place) predicate over class of relations),
(know what theorems can be used rele. to β, .40, .70, intu: find out β's type)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(intu, active transformation, (treat as an Op. on Actives, .5, ),
(intu, static,(treat as Relation or Property over Actives, high, ,)}
WORTH: high
BOUNDARY
DOMAIN/RANGE {not} {(the set AA of Actives -- or AAxAA, AA, operation)}
ORDERING(Complete)
WORTH (.6, .7, .5, .5, .6, .8, .7, (1.0 formal, .6 intu), .6, (1.0 basis))
INTEREST {(interesting as an Active), that level of int., direct),
(new theorems about Actives which satisfy this proposed property,
.6 + .4*(avg. int. of thms.), coincidences are rare and wondrous)}
OPERATIONS Actually coincides with this BEING itself; view as reln, so see reln.ops.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
REPRESENTATION
VIEWS {(as a relation, with (a,b) interpreted as meaning that the Active a (or --
the ordered pair of Actives a=(a↓1,a↓2)) is related to the Active b.)
(as a property, whose master set is all Actives AA; or, AA↑2. extend: consider AA↑n)
(as an operator, whose domain is AA or AA↑2 and whose range is AA.)
⊗5INFO GROUPING⊗*
DEFINITION An Active entity P which connects other Actives together.
View P as a pred.: For each Active R satisfying P, we say that R is P (P adjective)
or R has property P.
INTU View P as reln: Some tie, some common statement true of the Actives which have this property.
Similarities in details of the arrows which connect sets; a ⊗4type⊗* of arrow.
TIES Up: ACTIVE, Operations Archetypical BEING.
EXAMPLES {not} {bdy} Composition, Repeat. ←← probably these should be BEINGs themselves.
WORTH: huge variation, but usually quite interesting.
CONTENTS Compose, repeat, apply.
FILLIN: Use algorithm if it is fast and if domain is small enough.
Use thm. that reln. having prop. A, B,... must also have this property.
.SKIP TO COLUMN 1
⊗3STATIC META BEINGs⊗* Higher-level constructions.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (justif, quality, (absolute formal, pf or thm),
(high but intuitive or empirical, conjecture),
(mediocre but planned ephemerality, assumption),
(none needed -- existance, object))}
BOUNDARY {(boundary, dom/range meaningful, (static quality, destroyed)),
(justif, not needed, (belief, irrational (revelation-axiom, existence-object)))}
ORDERING(Complete)
WORTH (.5, .7, .4, .5, .6, .6, .5, (depends on specialized form: .1 to 1.0 spread
in both formal and intuitive), .4, (1.0 basis))
FILLIN: If used with only one BEING β, after enough time has elapsed take it
and make this just one subpart of TIES part of β. (saves time/space)
INTEREST This part is of course very important; it is the key to what to look for.
(Used in multiple proofs, by many other active BEINGs, to good advantage; .8,),
(Conjoins with another static entity to yield a very surprising result, .8,interest)
...
JUSTIFICATION
OPERATIONS Active META BEINGs, in general.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(if too active, replace by all int. static applications),
(if hard to justify yet crucial, ask if it can be assumed as an axiom)}
REPRESENTATION
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION Holder of information produced by active meta β, tying together lesser BEINGs.
INTU Facts ⊗4about⊗* the facts; results of using same.
TIES Up: Specific Knowledge BEING
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2STATEMENT⊗* An expression of some thought.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Object.
SPECIALIZATIONS {(justif, quality, (formal, theorem), (informal only, conjecture)),
(argument:structure, may as well be viewed as a set; ∀xε[Convert-to-set S].P(x)),
(format of the thought,
(∀ members of structure. P holds, Statement of Generality),
(∃ member of structure. P holds, Statement of Existence))}
BOUNDARY {(size of the structure S, empty, statement is vacuously true usually)}
ORDERING(Complete)
WORTH (.5, .8, .6, .4, .7, .8, .4, (both can vary highly), .5, (1.0 basis))
INTEREST This part is of course very important; it is the key to what to look for.
(It is surprising that the statement is true, raher than just a weaker version)
(What we really want is an easier result, but this "hard" statement is actually clearer)
JUSTIFICATION
OPERATIONS Prove, Disprove (if not already certain). Use (if reliable).
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION Formally, usually as a pc wff.
VIEWS A proposition, which should be closed (no free variables), which is menaingful.
An assertion of some relation holding in some way; often involving quantification.
This may be a fact about a given entity, about its subparts, about a pair of things, etc.
⊗5INFO GROUPING⊗*
DEFINITION An object which is clearly either true or false, typically having a meaningful
intuition, usually involving an Active, a structure, and one more structure
or Active BEING. The typical statement is a claim, an assertion of the form
that the Active applied to the structure either (i) satisfies the other Active, or
(ii) is equal to the other structure. Two common quantified forms of statements
are those of generality and those of existence; they have an Active P and a
structure S, and some other Active Q (either ∀ or ∃), and they claim that
P applied to a member of S satisfies the quantification property Q.
INTU See intu for quantif, for propostional constants, for conjectures, theorems, etc.
TIES Up: Static Meta BEING
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2CONJECTURE⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(a certain relnship is given a name and temp. β status, .80, .80, )}
FINAL
PAST {(want to prove something which currently is not a β of any kind, .70, .80,
intu: first isolate it, then study it)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (justif, quality, (empirical, may be coincidence, try to understand intu),
(intuitive, may be completely wrong: gather empirical evidence),
(almost syntacticly, from an anlogy, gather empirical evidence; hint: use ana. evid.))}
(none needed -- existance, object)),
(the type of the conjecture, the front quantifier,
(none, .50, declaration), (∀, .60, statement of generality), (∃, .55, statement of existence))}
BOUNDARY {(justif, quality, (high enough and formal enough, theorem)),
(none needed at the moment, assumption))}
ORDERING(Complete)
WORTH (.4, .8, .5, .5, .6, .7, .5, (formal: below .90, intu/empir: ≥.10), .4, (1.0 basis))
FILLIN: If unproven after enough attemps, after enough time has elapsed,
then this β can be destroyed (just record a few key loop-stopping facts)
INTEREST This part is of course very important; it is the key to what to look for.
(If this were known to be true, would it be interesting?, .9*that rating,)
...
JUSTIFICATION
FILLIN: see Specializations part; also, when nonformal is high enough, try to PROVE it.
OPERATIONS Prove, Disprove.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(-): (complete proof or disproof),(decide to assume it as basic)}
REPRESENTATION Formal language statement, possibly involving quantification.
VIEWS An unproven statement.
⊗5INFO GROUPING⊗*
DEFINITION A potentially true meta-fact, a tying of other β's, which is not yet reliable.
INTU Mountain-climbing: leader who must hammer in pitons himself to help followers.
TIES Up: Static Meta BEING, Statement Side: Object, Theorem, Proof, Counterexample
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2STATEMENT OF GENERALITY⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST {(want to prove something about all elements of structure S, .70, .80, intu: prove in parallel)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Statement.
SPECIALIZATIONS
BOUNDARY {(size of the structure S, small, no need for ∀ format)),
(of the form ¬∀<var>¬P(x), awkward to use ∀ instead of ∃)}
ORDERING(Complete)
WORTH (.5, .8, .6, .4, .7, .8, .4, (both can vary highly), .5, (1.0 basis))
INTEREST This part is of course very important; it is the key to what to look for.
(It is surprising that the statement is true for all members and not just some)
(There is one specific member whose proof we can't get; perhaps it is easier to prove ∀)
JUSTIFICATION
OPERATIONS Prove, Disprove (if not already certain):
If unproven after enough attempts, after enough time has elapsed,
then try proving the thing with ∀ replaced by ∃, try reworking intu, etc.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(-): (introduce one exception into S)}
(+): (remove all the exceptions from S), (if P involves ordering/next, then try rearranging S)}
REPRESENTATION Formally, usually of the format ∀xεS.P(x).
VIEWS A universally quantified sentence in the variable x.
A simultaneous assertion for each element of S.
Proving it in general: a model which could be used whenever you want, for any specific xεS.
Notice that this is a statment about the elements of S, more than about S itself.
⊗5INFO GROUPING⊗*
DEFINITION A statement that asserts that a certain property holds for each individual
member of a certain struc. That is, "P(x)" is a true assertion when x is replaced by
(the name of) any member of structure X.
INTU See intu for univ-quantif. Collective statement. Stereotype. Generalization.
Assertion of the P-indistinguishability of all members of S, their equivalence wrt P.
TIES Up: Statement Side: Universal-quantification
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2STATEMENT OF EXISTENCE⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST {(want to prove something about structure S, .60, .75, one of its abilities is...)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Statement.
SPECIALIZATIONS {(the actual satisfying ele. is known, say it is a. Then one can say P(a))}
BOUNDARY {(size of the structure S, small: singleton or empty, no need for ∃ format)),
(of the form ¬∃<var>¬P(x), awkward to use ∃ instead of ∀)}
ORDERING(Complete)
WORTH (.5, .8, .6, .6, .7, .8, .5, (both can vary highly), .4, (1.0 basis))
INTEREST This part is of course very important; it is the key to what to look for.
(It is surprising that the statement is true for any member at all in S)
(We really need only to show existence in some larger set, but we think that
it would have to exist (at least one such would exist) in this substruc S, and
also we think it might be easier to show ∃ here since S has some nice properties related to P)
JUSTIFICATION
OPERATIONS Try and construct the actual element x which satisfies P.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(+): (introduce one satisfying ele into S)}
(-): (remove all the satisfying eles from S)}
REPRESENTATION Formally, usually of the format ∃xεS.P(x).
VIEWS An existentially quantified sentence in the variable x.
A simultaneous disjunction with a disjunct P(x) for each element of S.
Proving that S can do the job, that it has a certain capability, that somebody in S can do it.
Notice that this is a statement about S, rather than about the elements of S.
⊗5INFO GROUPING⊗*
DEFINITION A statement that asserts that a certain property holds for some individual
member of a certain struc. That is, "P(x)" is a true assertion when x is replaced by
(the name of) some member of structure X. Not necessarily all members of S will
make P true, and we may not even be able to point to the satisfying member of S,
though of course that is one way of establishing (constructively) the existence.
INTU See intu for exis-quantif. Statement of ability to do the job; S is a room full
of specialists, and we are saying that S as a unit can do something.
TIES Up: Statement Side: Existential-quantification
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2THEOREM⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST {(want to prove something similar to this theorem, .60, .70,intu: either as
a model or as a tool)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (past, one big thm. uses this,
(as a stepping stone or as a tool, .60, called a "lemma")),
(type of front quantifer,
(∀, .8, a universal theorem, see statement of generality)
(∃, .75, an existential theorem, see statement of existence)
(none, .7, a true proposition, see propositional constant))}
(past, void, (no real usage --at least yet, .30, called "proposition")
IDEN: corollary
FILLIN: coincidence
WORTH: high
)}
BOUNDARY {(justif, quality, (not absolutely formal, conjecture),
(none present or needed, object))}
ORDERING(Complete)
WORTH (.7, .8, .6, .4, .5, .7, .4, (formal: 1.0, intu/empir: no constraint), .5, (1.0 basis))
INTEREST This part is of course very important; it is the key to what to look for.
... <I am unsure exactly what goes here that can't go at a higher level>
Unexpected, hard to prove,
Negative weight if obvious, expected, a trivial pf exists, vacuously true, etc.
Relates entities which are either diff or else already rel. in a very diff way.
(Past, heavy usage, .8, utility)
JUSTIFICATION Point to a proof for formal justification, and also indicate which
specific mathematical theory this was proven in (i.e., which axiom set and
derived theorem set was implicitly assumed as valid), and try to indicate the
full range of known mathematical theories in which the proof remains valid.
FILLIN: First attempt to find some intu, some empirical evidence, some ana.
WORTH: high
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(-): (conjoin new clauses to the theorem, (justif, no longer valid),
(+): (find a proof for an unproven statement, (justif, satisfied))}
REPRESENTATION Formal language statement, possibly involving quantification.
VIEWS A proven statement.
⊗5INFO GROUPING⊗*
DEFINITION A proven, true meta-fact, a tying of other β's, which is reliable, which
is equivalent to True, in some given mathematical theory (that is, it follows
logically from the set of axioms of the foundation of that theory).
In the course of proving this theorem, any auxiliarry result which is of
little outside interest but is a crucial step in the proof may be called a ⊗4lemma⊗*.
Typically, the theorem is a statement of the form "If P is true (about the
basis of this mathematical theory, and if we assume all the foundation axioms)
then Q is also necessarily true (about the structures and actives talked about
in the basis, or about entities built out of them). Usually, we omit the two
parenthesized phrases, but they are always assumed to be understood. We call
P the hypothesis, and Q the conclusion. Both P and Q should be statements.
P and, especially, Q are usually statements of generality or of existence.
INTU Mountain-climbing: safe, secure base camps, each one should be higher up.
TIES Up: Static Meta BEING Side: Object, Conjecture, Proof, Counterexample
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2PROOF⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(the truth of P is now made formally obvious and clear and believed, .90, .80,
intu: by looking closer longer, we can see more clearly and with more continuity),
(convince audience of truth of P, .85, .75, intu: lead flock down path)}
PAST {(working on an analogous task as this proof accomplished, .40, .50, intu: ana)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (worth, values become extreme,
(complexity drops to zilch, .20, triviality; easily rederivable if every needed;
suggestion: if this keeps recurring, let it exist; else forget it and/or demonize),
(complexity is too high, .20, find quasi-interesting resting-palces along the
route, a sequence of lemmas, to aid in comprehension and later analogies)),
(contents, value filled in or not, (exists constructively or not, .60/.50,
affects what you can do with this, what kind of handle there is on it))}
BOUNDARY {(justif, quality, (not absolutely formal, sketch of a proof),
(none present or needed, axiom))}
ORDERING(Complete)
WORTH (.5, .4, .5, .6, .7, .9, .3, (formal: 1.0, intu/empir: no constraint), .2, (1.0 basis))
INTEREST This part is of course very important; it is the key to what to look for.
There may in fact be no reason why a ⊗4proof⊗* is int, although the fact that
one ⊗4exists⊗* for y (ie., that y is a theorem) may be quite interesting.
... <I am unsure exactly what goes here that can't go at a higher level>
(Past, heavy usage, .8, utility)
JUSTIFICATION Each entry has its own justification from thms, axioms, rules of
inference, and earlier entries (including earlier assumptions if they are
maintained explicitly as such).
FILLIN: Attempt to find some intu, some empirical evidence, some ana.
Analyze the structure of the desired theorem; is it univ or exis?
In general, ask the PROVE active-meta-BEING to do this.
WORTH: high; even though the contents are unint, their ∃ is important.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(+): (find a proof for any unproven intu. steps in sketch,
(justif, satisfied))}
REPRESENTATION (assertion, justification)* where each assertion is a mini-theorem.
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION A nonempty sequence of statements (about the basis and its superstructures),
each of which is either an axiom, an assumption, an earlier theorem,
or follows by a rule of inference from some axiom, theorem, or
earlier statement. The justif. for each statement is appended onto it.
Ultimately, any assumptions which cannot be discharged are conjoined into the
hypothesis of the theorem which has been created, and any interesting statement
in the proof (usually the final one) is taken to be the conclusion. One may
then assert that the theorem <hypothesis> → <conclusion> has been proven.
if P is not identical to this, it might be a quick corollary. If P (of the form A→B)
must be equal to this, then we must not stop until one of the statements in the
proof is B, and until all the assumptions not in A have been discharged validly.
Thus one could view a proof as a list structure, a list each of whose
elements is an ordered pair (s,j), where j proves s; in this recursion, a
primitive proof is (axiom,PHI) or (theorem,PHI) or (previous s,PHI) or
"rule of inference r applied to axiom α and theorem β with x replaced by SET..."
etc. The big difference here is that the ⊗4contents⊗* of the structure
are of central importance, whereas for pure structures that is irrelevant.
Thus no "syntactic" definition should be alone here; a "semantic" one is a
practical necessity.
INTU Mountain-climbing: the trail to the summit (distinct from the summit itself of course).
A new floor in a building; each new step (statement) in the proof is a supporting
part (e.g, beam, wall). The assumptions are like the scaffolding.
TIES Up: Static Meta BEING Side: Object, Conjecture, Theorem, Counterexample
EXAMPLES {not} {bdy} (Bdy,+, axiom)
CONTENTS
.SKIP TO COLUMN 1
⊗2COUNTEREXAMPLE⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST {(working on an analogous task as this disproof put a stop to, .40, .50, intu: ana)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY {(justif, not absolutely formal, (justif, must be made ironclad))}
ORDERING(Complete)
WORTH (.3, .4, .6, .5, .6, .7, .4, (formal: 1.0, intu/empir: no constraint), .2, (1.0 basis))
FILLIN: If only the existence of the counterexample is of any int, or esp.
if the non-thm. itself is no longer of any int., then forget all about this β.
INTEREST This part is of course very important; it is the key to what to look for.
There may in fact be no reason why a ⊗4counterex.⊗* is int, although the fact that
one ⊗4exists⊗* for y (ie., that y is not a theorem) may be quite interesting.
... <I am unsure exactly what goes here that can't go at a higher level>
(Past, heavy usage, .8, utility)
JUSTIFICATION An object or relationA justification from thms, axioms, rules of
inference, and earlier entries (including earlier assumptions if they are
maintained explicitly as such).
FILLIN: Attempt to find some intu, some empirical evidence, some ana.
Analyze the structure of the desired theorem; is it univ or exis?
In general, ask the PROVE active-meta-BEING to do this.
WORTH: high; even though the contents are unint, their ∃ is important.
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(+): (find a proof for any unproven intu. steps in sketch,
(justif, satisfied))}
REPRESENTATION (assertion, justification)* where each assertion is a mini-theorem.
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION A sequence of statements, each of which is either an axiom, an earlier
theorem, or follows by a rule of inference from some aiom, theorem, or
earlier statement. The justif. for each statement is appended onto it.
Thus one could view a proof as a list structure, a list each of whose
elements is an ordered pair (s,j), where j proves s; in this recursion, a
primitive proof is (axiom,PHI) or (theorem,PHI) or (previous s,PHI) or
"rule of inference r applied to axiom α and theorem β with x replaced by SET..."
etc. The big difference here is that the ⊗4contents⊗* of the structure
are of central importance, whereas for pure structures that is irrelevant.
Thus no "syntactic" definition should be alone here; a "semantic" one is a
practical necessity.
INTU Mountain-climbing: the trail to the summit (distinct from the summit itself of course).
TIES Up: Static Meta BEING Side: Object, Conjecture, Theorem, Counterexample
EXAMPLES {not} {bdy} (Bdy,+, axiom)
CONTENTS
.SKIP TO COLUMN 1
⊗2CONTRADICTION⊗* Notice that this might be tied into the environment (belief)
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS disproof of x
BOUNDARY {(where the assumption came from: (the user, .8, a joke),
(the negation of a desired conjecture, .85, a formal indirect proof),
(no assumptions made, .98, an inconsistency in the zxioms of the current
mathematical system being developed; all the theroems are thus only vacuously true;
this is very dangerous and very displeasing, but motivation exists to remedy it,
typically by modifying the set of axioms; try to explicate which are not independent))}
ORDERING(Complete)
WORTH (.2, .5, .5, .5, .6, .7, .4, (formal: 1.0, intu/empir: suspicious), .1, (1.0 basis))
FILLIN: Generally, one will destroy the entire world wherein this is found to occur!
INTEREST The establishment of the contradiction proves that one of the assumptions
made is false, which may lead to an interesting theorem.
JUSTIFICATION The justification, while syntactically identical to that for a proof,
is semantically understood to follow from false assumptions, hence is trivial.
FILLIN: Consider how to find a proof of a false statement.
In general, ask the PROVE active-meta-BEING to do this.
WORTH: high; even though the contents are unint, their ∃ is important.
OPERATIONS Understand its origins, try to resolve it
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION (assertion, justification)* where each assertion is a mini-theorem
or an assumption (absolute justification or none whatsoever).
VIEWS (as a proof technique: indirect proof of Y: assume ¬Y and derive a contradiction)
⊗5INFO GROUPING⊗*
DEFINITION A situation where assuming x leads to the proof of a false statement.
Often this is done by proving ¬x and then concluding x ∧ ¬x, which is = F.
The fact that x → F means that x itself must be false. Here x is the conjunction
of all the assumptions which had to be made before the proof.
When we say that x is impossible, we mean that oneor more of its conjuncts are.
Typically, one can say that the system enters a hypothetical world by assuming
x, then shows that the world is inconsistent, then destroys that world but
retains the fact that x can not possibly be true. Thus ¬x is proven as a theorem.
If x is believed, reexamine those beliefs until the belief level of x drops.
As a last resort, consider restricting the methods used in the proof, of redefining
some of the concepts so that the contradictory proof can never be done legally anymore.
No "syntactic" definition should be alone here; a "semantic" one is a
practical necessity.
INTU It can't be so; if it were, nothing would make any sense.It is a paradox, a joke.
TIES Up: Static Meta BEING Side: Indirect proof
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2BUG⊗* The only other type of known error, except for Contradiction.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(perfection of piece of knowledge/code, .70, .75, repair)}
FINAL
PAST {(error message from system: interrupts go here, .80, .85, alterations of clothes)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Error, contradiction, problem with internal model of the world.
SPECIALIZATIONS
BOUNDARY
ORDERING
WORTH (.1, .4, .4, .5, .6, .5, .4, (formal: empirical; intu: fallability), .1, (1.0 basis))
FILLIN: Generally, one will work until the bug goes away, then let the new bug β die.
Retain, however, some idication of its origin, in the form of a demon to watch
for similar situations in the future, and also one to handle those that slip by.
INTEREST
JUSTIFICATION The only justif. is the operating system and the formal syn. of LISP.
WORTH: low; only the existence counts.
OPERATIONS Debug: work on the triggering entity until it no longer triggers.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} Debug
REPRESENTATION (type of bug, pointer to trigger, description of origin, how to fix)
VIEWS (as a communication between the system and the operating-system)
(as a contradiction between the way the sys. thinks the trigger is, and the way it is)
⊗5INFO GROUPING⊗*
DEFINITION A situation where a trigger x leads to the inability to do what the sys. thinks is
doable. This might be applying an op. to something thought to be in its domain,
accessing something which in reality can't be accessed, carrying out something
which has no definition known to the operating system, etc.
No "syntactic" definition should be alone here; a "semantic" one is a
practical necessity.
INTU It can't remain as it is; either decide to try to fix it or forget the triggering action.
Clothes don't fit. Engine malfunction. Misjudgment.
TIES Up: Static Meta BEING Side: Contradiction
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2ANALOGY⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(statement involving x → involves y, .70, .80, )}
FINAL {(clarify ties between x and y, .60, .70, )}
PAST {(looking around, trying to decide what is plaus. to say about x, .60, .75,)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS relation
SPECIALIZATIONS {(defn/intu, strengthen, (no functional diffs. at all, equivalence),
(contents, completeness, (maximal -- to the point of flawless structural
equality and truth preservation under any applicable relation, .90, isomorphism))}
BOUNDARY {equivalence; no similarity of any power is ever found}
ORDERING(Complete)
WORTH (.6, .9, .6, .5, .5, .6, .4, (formal: often low, intu/empir: ≥.10), .8, (1.0 basis))
FILLIN: If no uses after enough attempts, after enough time has elapsed,
then this β can be destroyed (just record a few key loop-stopping facts)
INTEREST This part is of course very important; it is the key to what to look for.
(If this were known to be true, would it be interesting?, .9*that rating,)
(Say P(y) is v. int; P(x) would be v. int, but it is hard to see how to
prove or even intu. interpret P(x); then look for ana. y↔x; .9*int of P(x))
(Two BEINGs which seem very diff. correspond under the analogy, .7)
If the ana. is based on the fact that the values of two equally-named parts are
equal, then the interest rating is exponential in the unusualness of that value.
For example, Unfilled-in has value 0; T or F have value 1; the list
(3 5 7 11 13 15 2) has value 8; a member identified as from a set of k
equal possibilities is granted usualness k. The correspondonding interest
values for an ana. based on these would be 0, 1, 64, k↑2.
Notice the interesting case when x and y are both analogies themselves!
If Ana. seems strong, then suddenly propsoition P is found which was expected to
be universal but is found not to be, then it may be very interesting to study
.ONCE TURN ON "[]"
the two subsets P↓[yes] and P↓[no] on which P actually does hold (fails).
...
JUSTIFICATION
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(-): (formal, absolute proof of the ana., defn, equivalence),
(+): (Serious flaw in that P does not carry over; modify x into a new β which
⊗4does⊗* satisfy P; try to maintain all other existing ana. strengths)}
REPRESENTATION (part, how to make things related to this part of an x correspond to
things related to this part of a y, vice versa, strength, interest)*
VIEWS (As a relation, mapping β's into somewhat similar β's),(As a conjecture with
many component assertions)}
⊗5INFO GROUPING⊗*
DEFINITION A potentially useful correspondence between two β's, which is more than coincid.
A correspondence between the properties of two ideas, typically high intu. clarity.
An analogy is called ⊗4partial⊗* if not all parts of each map into anything;
it is called ⊗4weak⊗* if there is more than one way to map a given part.
(A weak analogy should be strengthened or split into separate analogies)
INTU Mountain-climbing: try and find a path someone already hacked out, even if slight detour.
Two different views; in any given sit, can use the one which is best suited.
TIES Up: Static Meta BEING Side: Conjecture
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: Try to extend this to as many parts as possible, as certainly as possible.
.SKIP TO COLUMN 1
⊗2MESSAGE⊗* A structured communication (BEING↔BEING or user↔BEING)
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(destination receives the given info, .80, .80,intu: on target)}
PAST {(x wants to communicate i to y, .90, .80,)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(contents, complexity, (low enough, .90, simple BEING part call))}
BOUNDARY {simple part call; new permanent β desreves creation}
ORDERING(Complete)
WORTH (.3, .2, .01, .4, .7, .5, .3, (formal: often low, intu/empir: ≥.20), .5, (1.0 basis))
FILLIN: In almost all cases, after successful transmission, this will be
forgotten. Thus all instantiations have final component (0.1 NIL).
INTEREST The receiver does not know the given information; it will change his behavior;
There is difficulty in communicating this, but sender thinks it is important.
Probably forbid the case when x and y are both messages themselves!
JUSTIFICATION
OPERATIONS Communicate
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(-): (well-interfaced directly into part of receiver),
(+): (Difficulty occurs while trying to send part of y what was thought to be
a routine transmission)}
REPRESENTATION (part, examples of changes which should be made, intu of these changes)*
VIEWS (As a relation, handling awkward interfacing between β's),(As an object,
passed between BEINGs)}
⊗5INFO GROUPING⊗*
DEFINITION A structured attempt to overcome a difficult family gap and transmit info in such
a form that anybody who should have it might assimilate it successfully.
This stresses the intuitive and exemplary modes of information specialization
by the sender, followed by the receiver guessing the info from such clues.
INTU Two people speaking different langs. communicate via pointing, gestures, and pictures.
TIES Up: Static Meta BEING Side: Communicate, Object
EXAMPLES {not} {bdy}
CONTENTS
FILLIN: If the exs. and intu. are not developed, try to do that at this point.
.SKIP TO COLUMN 1
⊗2ASSUMPTION⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(x goes instantly from unknown to true, but only temporarily, .80, .80, )}
FINAL
PAST {(proof by cases in progress; assume each in turn, .70, .80,
intu: all roads diverge here but meet again at a point further on),
(To find interesting x→?, assume x and see what int. facts now can surface,
.60, .50, intu: to see consequence of x, enter the world where x is true)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(worth, justif, (exists, .80, conjecture),
(absolute belief eternally yet no esistence, .50, axiom))}
BOUNDARY {(worth/justification, quality, (high enough, conjec),
(absolute formal justif. exists, so eliminate this assumption entirely, thm))}
ORDERING(Complete)
WORTH (.4, .5, .5, .6, .5, .6, .5, (formal: temporary only, intu: unimportant), .1, (1.0 basis))
FILLIN: In all cases, after the ramifications of this assumption are studied,
it is forgotten. Thus all instantiations have final component (0.1 NIL).
INTEREST This part is of course very important; it is the key to what to look for.
(If this and its alternatives all lead to the same spot, we know we get there)
JUSTIFICATION Absolutely none. The motivation for ⊗4creating⊗* the assump. exists, however.
OPERATIONS Actualize: replace desired implicate I by "ASSUMP → I", absolute justif.
This elimination of assumptions turns the tentative result into a fact.
Of course, if the implicate used other assumptions, then the "fact" is still
just an implicate of those assumptions.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} {(-): (Accidentally find a proof or disproof, justif, exists)}
REPRESENTATION Formal language statement, possibly involving quantification.
Some special tag to indicate Assumption.
Probably every "fact" should point to its assumptions, in the Justification part.
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION A hypothetical world is entered where this is true; we must eventually come back.
INTU Pondering the alternatives before deciding which to actually undertake.
TIES Up: Static Meta BEING Side: Object, Conjecture, Proof.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2MATHEMATICAL THEORY⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
BOUNDARY
ORDERING(Complete)
WORTH (.9, .9, .1, .9, .6, .9, .3, (formal: must be present, intu: hopefully), .1, (1.0 basis))
INTEREST This part is of course very important; it is the key to what to look for.
One must look for very useful and/or interesting examples of and instances of the theory.
The use in such cases: First, this points out kinship between otherwise apparently dissimilar β's.
Second, great economy of effort comes from deriving properties from axioms of the
system, hence true of each instance we can find.
Third, in case the axioms are categorical, the First advantage goes away,
but we gain the fact that any single instance is now prototypical representative.
JUSTIFICATION The foundation has only intu., the theorems have proofs (sometimes intu. as well)
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION (foundation, theorems)
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION An explicit choice of a foundation (a basis and axioms about the basis)
plus a body of theorems; each theorem is simply a statement of the form:
"if x is true of the basis, then it is a logical necesity that y is also true".
Each theorem must have a logically valid proof, and hopefully some interesting intuition.
Each piece of the foundation should have high intuition, but low intuition for major thms.
FILLIN: One technique is to take a series of related, specific examples,
and make them instances of one system, by abstracting their common properties
and postulating these as the axioms, abstracting their common basis.
This process is called unification. Another process is perturbation:
Take an existing Mathematical system and modify its Foundation.
INTU Some nodes and the arcs connecting them.
Executing a program: basis=pgm, logic=how to run a pgm, thm=result of one evaluation.
An edifice, built upon a foundation in accord with carefully prescribed construction codes.
A game: basis structures↔chess men; basis Active↔moving from one square to another;
foundation axioms↔starting configuration, leagal moves, rules of chess;
logic↔universally true rules about games, alternation of players, fairness;
theorems of the theory↔later configurations which can legally be reached;
interesting theorems↔positions reached when both players are experts;
defect in this analogy: there is no correlate to winning/losing.
TIES Up: Static Meta BEING
EXAMPLES {not} {bdy}
IDEN: referred to as ⊗4instances⊗* of the given theory.
DEFINITION: Interpret each structure and each operation of the basis in terms of
the real world or some other theory, in such a way that each axiom is
true (either intuitively, by assumption in the new system, or by proof),
and for which each rule of inference (each proof technique) is still acceptable.
VIEWS: As a map, similar to analogy.
INTEREST: Viewed as a mapping or analogy, this maps thms into (potentially new) thms.
EXAMPLES: [Each structure in the basis is interpreted as a real-world object,
each Operation is interpreted as a physical activity one can perform,
each Property and Relation interp. as a physical one (like "betweenness").]
CONTENTS
.SKIP TO COLUMN 1
⊗2FOUNDATION⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (Assumptions)
(The set of axioms is proven to be independent; do this by finding, for each axiom A,
an example in which A is false but all the other axioms hold.)
BOUNDARY
ORDERING(Complete)
WORTH (.4, .5, .5, .5, .4, .6, .5, (formal: assumed, intu: hopefully), .2, (1.0 basis))
INTEREST Each part is trivial intuitively, yet the resultant theory is interesting.
The int. is high if it is an abstraction of a useful real-world situation, where
the basis corr. to physical strucs and activities, and the axioms are
observed properties of those entities (from which all the already-known
observed properties can be derived).
In such cases, the int. is very high if some prediction is made and is
subsequently shown to hold in the intuitive, observable world.
The int. is very low if no non-vacuous example can be found after a few attempts.
In this case, it might be best to start trying to prove the axioms inconsistent.
A single, good, intuitive instance is quite adequate to prevent this doubt.
JUSTIFICATION Intuitive, usually; never any formal justification beyond that of assumption.
OPERATIONS One finds ties among the basis elements,
proves theorems about what they and the axioms imply.
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not} One construct can be formed out the others: superfluous.
REPRESENTATION (Basis, axioms)
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION An explicit choice of the subject matter of a mathematical theory,
by fixing a basis (some structures and some operations, with postulated properties of
each structure and operation) and a set of axioms, which together play the role of the known,
assumed, given knowledge for that theory.
Hopefully, each of these entities will have decent intuitions.
INTU The foundation for a building, plus building materials for the rest, plus raw
materials for building tools to help speed up the construction process.
TIES Up: Static Meta BEING, Mathematical Theory
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2BASIS⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Structure
SPECIALIZATIONS
BOUNDARY
ORDERING(Complete)
WORTH (.4, .5, .5, .5, .4, .6, .5, (formal: assumed, intu: hopefully), .2, (1.0 basis))
INTEREST Each is trivial intuitively, yet with a simple set of axioms, the resultant thy is int.
JUSTIFICATION Intuitive, usually; never any formal justification (strucs. are nonjustifiable).
OPERATIONS
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
REPRESENTATION Tagged collection of definitions of (and/or formats of)
structures, distinguished eles and subsets of them, and actives which work on
them and on each other. (That is, the domains of these Actives usually contain
some of these structures, their elements, or other actives).
For each we provide corresponding intuitions, all of which are to be assumed.
VIEWS
⊗5INFO GROUPING⊗*
DEFINITION An explicit choice of the subject matter of a mathematical theory,
by fixing some structures and some operations (with postulated properties of
each structure and operation) which are to play the role of the known, assumed, given
knowledge for that theory.
In addition, we distinguish some subsets of and elements of some of the structures.
Typicaly, these are just names and assertions of memebership/containmnt; the axioms
of the theory will help to specify the special properties which make them interesting.
Hopefully, most of these entities will have decent intus.
INTU The materials for the foundation for a building, plus raw materials for the rest.
TIES Up: Mathematical Theory, Foundation
EXAMPLES {not} {bdy}
CONTENTS
⊗2FORMAL SYSTEM⊗*
Not clear that this is really going to be any different from "Mathematical Theory" β.
.SKIP TO COLUMN 1
⊗3ACTIVE META BEINGs⊗* Actions which affect BEINGS
⊗5RECOGNITION GROUPING⊗*
CHANGES {(fill in (more of) a static meta-β, .80, .90, intu:fruit of the labors)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗* It is not clear whether any ⊗4new⊗* β's in this category will ever be created.
GENERALIZATIONS
SPECIALIZATIONS {(justif, degree of formality maintained,
(absolute, .70, math.induction/prove/disprove),
(minimal, .70, communicate/guess)),
(domain/range, restricted to known type of entity,
(conjecs → thms, .80, prove) etc),
(orientation, problem, (to prove, test), (to find, search))}
DOMAIN/RANGE {not} {(some β's (esp. static meta β's), a static meta BEING, op)}
ORDERING(Complete)
WORTH (.5, .4, .4, .5, .6, .7, .5, (both intu and formal vary widely), .5, (1.0 basis))
INTEREST (Its final product is going to be interesting if this succeeds)
OPERATIONS Execute them ←← probably implicit in the environment.
⊗5ACT GROUPING⊗*
ALGORITHMS
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Activities which result in the creation of orginal static meta β material.
INTU Ways to get things done, things to try, tools to produce finished products.
TIES Up: Specific Knowledge BEING Side: Relation, Static Meta β
EXAMPLES {not} {bdy}
CONTENTS Not clear that these β's will ever have Contents in any meaningful sense.
.SKIP TO COLUMN 1
⊗2FIND⊗* Search for a member of a space satisfying some desired criteria.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(given y in given S satisfying given P, .90, .65, intu: direct from defn)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(Knowledge about the space can be emplyed to advantage,
(there is a notion of a distance which can be used to gauge progress toward the
goal, .90, hill-climbing; intu: getting hotter/colder in finding-object game),
(the space is ordered, and some estimate or approximate starting point in the
search can be computed, .85, prediction/correction),
(the space is tree-like: make one choice out of a few, the result of which determines
the next few to choose from, .85, factoring the problem),
(the property P is satisfied by a special type of subspace: empty, all, computed)),
(all such elements are wanted, same as finding a specified subset of a given set)}
BOUNDARY {(the space is empty or universal; the criterion is trivial wrt the space),
(the space is the space of statements, the criteria is truth/belief, .90, proof)}
DOMAIN/RANGE {not} { (APRED x APRED, AO satisfying first predicate,op) }
ORDERING(Complete)
WORTH (.4, .5, .3, .5, .5, .5, .6, (1.0 formal, .7 intu), .7, (1.0 basis))
INTEREST When the desired kind of object is found, something good will have been done.
Difficult yet doable; utilizable later (interesting consequences).
Unusual properties of the space, esp. wrt the criteria, make the search one of computation.
OPERATIONS Show unsolvable: consider disproving, when it is viewed as ∃y.P(y).
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS Identify the space S. (intu: if S is too big, work first on a nice, small
subset of S, eg by using coincidences between parameters of S).
If S is explicitly generable, you are doing Select; if not, you are dealing with
the implicit structure defined only by the first argument, a predicate.
Devote some small time to ordering S so its eles. will emerge in some good order.
This is usually more costly than it is worth.
Ask struc for one ele x (if none, fail), if ¬P(x), then delete x and repeat.
If found, keep the partially depleted S around, in case another x must be found.
In fact, another algorithm (for another interpretation) is to find all such
x in S which satisfy the property, and keep this around. This may be faster
than the first algorithm even if only a few are wanted, if S is small enough.
Identify what the given parts are, and what the unknown which must be found is.
Pull out all the relevant facts (ana, ties, patterns, records of similar tasks).
For each similar task: can the method which was used be of any help?
Can the result which was found be of any help?
If it failed, how can I keep from making the same mistake(s)?
Reconcile the various views (intu, formal, etc). Problem→intu→soln.
WORTH: high
FILLIN: User provides a poiinter to very fast versions, but should still understand how.
REPRESENTATION
VIEWS (as finding a desired solution subset, a singleton substructure of a given struc)
(as constructively obtaining the element guaranteed to exist by ∃yεS.P(y))
⊗5INFO GROUPING⊗*
DEFINITION Examine the elements of a structure until we find one which passes a given test.
Failure means that there is no such element. Sometimes we want ⊗4all⊗* such eles.
INTU Walk through world, tagging until some the treasure is found.
If you can get some direction info. from your mistakes, this is tremendous advantage.
This will depend partly on type of struc (order? formatted?) and on criteria.
TIES Up: Operation/ Active Meta BEING. =:Problem-to-find. Side:Problem-to-prove.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2SELECT⊗* Choose one thing from among an explicit collection.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(change a set of alternatives into a single choice, .90, .85, choose)}
FINAL {(an element of, some member of, a given struc .80, .85, intu:choose from)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(The choice set is not known explicitly, .60, Find),
(The set contains Actives, meta-actives, and evaluable forms, .60, Control decision)
(The set contains alternatives to investigate, .60, focus of attention)}
BOUNDARY {(the space is empty or singleton: the result is trivial)}
DOMAIN/RANGE {not} { (ASTRUC x AOP (x Aordering β over Range(Op)), AO in the struc,op) }
ORDERING(Complete)
WORTH (.4, .5, .3, .5, .5, .5, .6, (1.0 formal, .7 intu), .7, (1.0 basis))
INTEREST When the desired kind of object is found, something good will have been done.
Difficult yet doable; utilizable later (interesting consequences).
Unusual properties of the struc make the search one of computation.
OPERATIONS When one crosses this into itself, one gets the idea of simultaneously
making choices from various specified structures. This leads to the idea of the
Principle of Choice; it is easier to grasp if the idea of singleton is already there.
(i.e., if the idea of a function is already there)
⊗5ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS The structure is gone through, and we return the member giving the best
performance wrt criteria specified in the operation (the second argument).
Best means the extreme, the greatest, wrt the ordering (usually implicitly)
defined on the range of the evaluation operation supplied. Said operation must
be applicable to each member of the structure; if not, it can be extended by
defining it to have a value which is a Least of the range of the operation.
At each moment, keep a record of the best candidate, stored in the variable BEST↓S.
The loop consists of repeatedly asking S for Some-member, then comparing the result
(its value under the Operation) to the current value of (the op applied to)
BEST↓S. The preferred entity of this pair is then stored in BEST↓S.
Delete the some-member from S, and repeat the loop. The loop terminates when
Some-member canot find any more mebers, at which time we return BEST↓S.
Sometimes, the current value of BEST↓S will indicate whole substrucs knwon to be inferior,
will indicate sterner comparison criteria (speed up the operation algorithm)
Example: αβ searching
Sometimes, we may want to later find the next best member; in such cases, it is
best to simply order the structure S according to the ordering induced by
the ordering on the range of the evaluation operation; then the best one in S
is the First one; removing it makes the best one the First one of the remainder, etc.
FILLIN: User provides a pointer to very fast versions, but should still understand how.
REPRESENTATION
VIEWS (as Finding a desired solution subset, a singleton substructure of a given struc)
(as Find in general, with correspondence of Structure↔predicate defining that struc)
⊗5INFO GROUPING⊗*
DEFINITION Examine the elements of a structure and find the one which is best for a certain
purpose (gives the extreme best values wrt a given evaluation operation).
FILLIN: One decsion which must be made is what to do if some elements are tied in value.
Alternatives are: pick one at random, pick first one if S is already ordered,
return all of them, apply a secondary ordering operation.
INTU Walk through finite part of world, tagging the best thing you've seen so far,
until everything (which might be the winner) has been inspected. Then pick the tagged item.
If you can get some direction info. from your mistakes, this is tremendous advantage.
This will depend partly on type of struc (order? formatted?) and on criteria.
Strong analogy with uniprocessor limitations; inability to do or concentrate on
more than a single thing at one time leads to the need to choose the best thing
out of all the possible alternatives. The idea of several comptetitors for one slot.
An election. The idea that a group of 200 works less efficiently than 200
workers toiling individually.
TIES Up: Operation/Active Meta BEING. Equivalent β: Problem-to-find, Find
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2GUESS⊗* Creatively produce a new conjecture, perhaps answering a given query
This actitivty might be distributed among the parts of "Conjecture"
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(if x can be shown to hold, then the given question q is answered, .60, .60,),
(the proposition x is interesting in its own right and should be studied, .70, .70,)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(results, justification, (nonexistent, .20, random or assume),
(absolute, .70, formally derive, prove))}
DOMAIN/RANGE {not} {(world examination, a conjecture, a pastime),
(question/uncertainty, a conjecture which immediately would anser the query, op)}
ORDERING(Complete)
WORTH (.4, .5, .4, .5, .5, .6, .4, (formal: low, intu: usually high), .5, (1.0 basis))
FILLIN: Even if the action of guessing warrants a new β, that β is deleted
as soon as the conjecture is well-formed; the only exception might be
if several alternative conjectures must be sifted through in some order.
Even in such a case, the actual guessing process would soon die.
INTEREST (More than one path leads the same way; e.g., analogy and empir. evidence)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here, I suppose, go all the hints for making new conjectures.
Pick a nice thm P(x) involving x; pick a nice analogy A from x to y; conjec. P(y).
Consider the empirical evidence and try to find a regularity in it; standard inference.
In response to a question, try to specialize the question, answer it
(perhaps via examples), then generalize the answer; or: use ana,
solve analogous problem, then map back using the same analogy.
The less sure x is, the less motivation we have to work on something which depends on it.
The less int. x is, the less motivation we have to work on something which depends on it.
Try to formulate the conjecture into a formal, crisp, clear statement of something
which must be proven (or, something which must be found).
Equally important is to get an intuitive procedure for recognizing what this means.
Sometimes the conjecture willnot be fully developed before trying to test it;
let the empirical evidence and the result of the test help to fill in the
variables in the statement of the conjecture. I.e., don't commit yourself to
proving x; rather, say you want to prove x(i,j,k) for some i,j,k, and then let
the proving itself help suggest what values for i,j,k woudl make it true.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Informal activities which result in the creation of new conjectures,
often to satisfy some specific need, some specific hole in a theory.
INTU Bet, choose, select candidate, then prepare to test him out.
TIES Up: Active Meta BEINGs Result: Conjecture Side: Assume
EXAMPLES {not} {bdy}
CONTENTS During activity, may include tentative conjecture; when conjecture is finally
revealed, this part may hold special info relating to what to do in case it
is shown not to hold, also how to answer originl question if it ⊗4does⊗* hold.
.SKIP TO COLUMN 1
⊗2ELLIPSIS⊗* And so on; ...; extrapolate; infer from examples.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(one more term is known in this sequence..., .80, .80, intu: inertia)}
FINAL {(find the pattern which produced this sequence..., .80, .70, synthesis)}
PAST {(many sim. sits. in pastand probably in the future, .85, .70, ibid)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS (S is ordered, and we provide a sequence of algorithms A,B,C,..., where
A is capable of producing First(S), B can produce Next(First(S)), etc, and we
must also provide a meta-algorithm R which can generate the next algorithm, given
all its predecessors, .60, )
SPECIALIZATIONS {(purpose of the sequence,
(to define a concept, .65, recursive or inductive definition),
(to communicate a message, .60, sign language; inferring from examples),
(part of reality, .70, guess: notice regularity in nature and transform into a conjecture))}
DOMAIN/RANGE {not} {(a structure (usually a sequence) of structured entities, a
procedure for obtaining the next member, synthesis of a simple algorithm),
(a structure of structures, the next member itself, extrapolation op.),
(structure x next-membr generator, {T,F}, pred: can this generate the struc?)}
ORDERING(Complete)
WORTH (.4, .5, .5, .4, .6, .5, .3, (formal: often low, intu: may be high), .5, (1.0 basis))
INTEREST (More efficent to store a short algorithm rather than a long sequence of outputs)
(If a regularity is noticed empirically, then it can be cast as a conjecture to be proven)
OPERATIONS Empirically check.
⊗5ACT GROUPING⊗*
ALGORITHMS Here, I suppose, go all the hints for inferring the next element of a struc.
Pattern-matching: try to compare each ele. to its successor; look for a known reln.
Cycles: split the sequence into subsequences by extracting every n↑t↑h element
starting with the k↑t↑h to get n different (k=1,2,...,n) subsequences.
Mapstruc: Apply an operation sequence-wide,
often not just to each ele. x but to the pair (x,Next(x)).
Compose: Do several of the above, several levels deep if need be, repeating until analyzed.
Synthesis: Once the pattern is analyzed, invert each step to build up an algorithm to reproduce it.
Intuit: Find a real-world situation with a sequence coinciding with this one,
then find the next element in the real world and return it (unjustified).
Example: Fibonacci sequence can be modelled by breeding rabbits.
Recursive definition: If S is an ordered structure, then it suffices to state
First(S), Next↑*(First(S)) for some initial sequence, and then to
give a rule for how to compute Next(x), given that the head of S is
(a b c ... x). Of course, one might break this into cases (e.g., cycles).
REPRESENTATION If the algorithm is known, store it and enough starting values;
if the pattern can't be deduced, store what is known already about elements of S.
VIEWS As set-difference: first arg is all possible elements, second is the given ones S;
task is to find elements not already found yet: in first arg but not in second.
⊗5INFO GROUPING⊗*
DEFINITION Given S, Find an algorithm A which produces Next(x) given any x in S,
except Last(S) of course, and try to extend S by postulating that it also works
for Last(S), to produce the next (unseen) element of S.
For this purpose, the algorithm should be compact and general and simple.
Alternatively, we just want Next(Last(S)) in any way; if S is a set, defined by
property P, and we are given some subset S', our task is to find some element
of S (something satisfying P) which was not included already in S'.
INTU Inertia, continuing in motion along the same direction(↔alg).
TIES Up: Active Meta BEINGs
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2ANALOGIZE⊗* Creatively produce a new analogy.
This actitivty might be distributed among the parts of "Analogy"
⊗5RECOGNITION GROUPING⊗*
CHANGES {(clarify ties between x and y, .80, .85, intu: an ana. is a sort of reln.)}
FINAL {(a new mapping is seen (a new ana. β) between x and y, .90, .86)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS fill in a new TIE
SPECIALIZATIONS conjecture structural isomorphism
DOMAIN/RANGE {not} {(AB = any BEING x AB, a new analogy Being),
(AB, AB, an operator which indicates the analogous BEings to the given one)}
ORDERING(Complete)
WORTH (.5, .5, .3**(no. of unspecified arguemnts + 1), .5, .7, .6, .3,
(usually one is high, other low), .4, (1.0 basis))
INTEREST (The two proposed analogous β's are highly structured, .7)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here, I suppose, go all the hints for making new analogies.
Choose the two candidate BEINGs. Some possibilities:
Pick a high-int. thm; look for syn. sim. thms; corr. subparts may be ana.
See if examples parts of 2 int. β's intersect.
To get the first β, do a specific lin. combo. sort on Worth of all β's,
include factors for how many parts are already filled in,
how many ties there are and how interesting they are.
If x,y are ana, consider ana. between the specializations or generalizations.
Consider the case of an anlogy from a BEING to itself.
This is termed: finding regularity within a BEING.
Two parts may be related in an unusual way.
Some unusual pattern may recur in many parts, in various shades.
Second order: if a β seems promising momentarily then is seen unacceptable,
record why. If later in this search you find one which fails
for similar reasons, that alone might be the basis for an ana. betw. them.
Locate other β's withsimilar set of parts filled in, similar ties.
Search through the responders if not too many, compare their values
Especially: intuition compatibility
Grow ripples from intus, until nontrivial ∩.
Create a new β, an analogy, between the 2 candidate BEINGs.
Modify CS to indicate the desirability to fill in this analogy.
Collect the facts about each; the parts, the ties.
Consider spending a little energy to complete parts of each β.
For each corr. pair of parts, try to find some ana.
An ana. between a pair of parts is either syntactic, usage, or meaningful.
A usage ana. means that there are thms and conjecs which are syn. ana.
A meaningful ana. is one which is understandable by one or both intus.
(betw. intu. parts: meaningful ana. means ripples of images interesect)
Extend an existing analogy
For each tie of one, conjecture an ana. tie exists on the other one.
Domain-independent: if two parts are often analogous, see if they are here.
Esp: parts with the same name.
Exploring regularity found within a single BEING.
Conjecture: a reln R holding on one part extends to hold on another
Conjec: a pair of conjecs, holding on sim. parts, are themselves related.
Can a more efficient repr. be found to eliminate or take advantage of duplicity?
Refine an existing analogy: find contrasts between he two analogous BEINGs.
Find parts on one which absolutely have no analogue in the other one.
Find parts which should be connected, but whose values in examples don't seem to be.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Informal activities which result in the creation of new analogy,
often with one or both candidates prescribed in advance.
INTU Notice similarity, superimpose potentially similar entities to more clearly
highlight the similarities and differences and distortions.
TIES Up: Active Meta BEINGs Result: Analogy
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2CONSERVATION⊗* Inertia; frame problem; invariance; compressability.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(antithesis; x should ⊗4not⊗* change, .90, .85, intu: keep x fixed)}
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS conservation of inertia, invariance, incompressability.
DOMAIN/RANGE {not} {(AB = any BEING, {T,F}, predicate: whether conserve(ed)(able)),
(Active x AB, {T,F}, pred: is the β conserved during the Active, or can it change),
(active, AB↑*, op: list of variants(or invariants) under a given activity)}
ORDERING(Complete)
WORTH (.6, .6, .1, .6, .7, .4, .1, (formal: ?, intu: usually high), .3, (1.0 basis))
INTEREST (One wants to do x and y simultaneously: make sure one is not changed
while achieving the second of these)
(Important savings later if we don't have to re-establish that one condition still holds)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS
Of inertia: if there is no evidence to the contrary, things continue once begun.
Exception: friction (must constantly supply some activities with supportive energy);
finite activites automatically end at next consciousness.
Frame problem is handled in this manner;
truth has such inertia, the same as any other property.
Invariance ←← perhaps this should be a part of every BEING!!
List of things which have no effect on this BEING; list which do change it.
If only one of these is manageable, mention this in place of the other one.
Reaction to stress
Elasticity: under slow, sustained effort, will this slowly change?
Plasticity: under rapid, sharp force, will this suddenly shatter?
Compressability: how much alteration can this take before breaking?
Fluidity: will this change of its own accord in some manner if not prevented?
Catalysts: Is there any aux. condition which dramatically affects its variablility?
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION The absence of change in x, even when the state of the world does change.
The precise invariance will depend on the entity. Even properties, such as
truth, are advantageously viewed as being invariant except in certain cases.
Result: Preservation of some substate of the world.
INTU Unrelated action; ability to withstand a force; rigidity, elasticity,
plasticity, compressability, fluidity, durability.
TIES Up: Active Meta BEINGs
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2EXAMINE⊗* prior to attemping pf. or disproof; which is more likely?
This is probably incorporable into TEST; if not, decide so during hand simulation.
.SKIP TO COLUMN 1
⊗2TEST⊗* Settle a claim. Prove or disprove a conjecture.
⊗5RECOGNITION GROUPING⊗* A conjecture x exists and is being concentrated on currently.
CHANGES {knowledge of the reliability of x increases, .90, .85, )}
FINAL {(truth of x is known, .90, .80,)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (Result, mode of certainty, (true: theorem, .90, prove),
(false, .70, disprove))}
DOMAIN/RANGE {not} {(a conjecture, dispf. or a proof, an operator)}
ORDERING(Complete)
WORTH (.7, .8, .6, .5, .7, .6, .5, (formal: 1.0, intu: decent), .4, (1.0 basis))
FILLIN: During the examination, a new β will probably be created. To avoid
clutter, once it is begun the effort to complete the testing will
be sustained at a nearly uninterruptable level. When it finally
succeeds or fails, the result may be saved as a new β, but the
process-of-testing β will die (except: possible retention for
use as a model for future tests iff it was very distinctive)
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Try to demonstrate which of {T,F} the argument is equivalent to.
There are two separate activities, that of proving and disproving.
What this BEING must do is choose which is more reasonable, and call on it.
For this decision, examine the empirical evidence, try to extend analogies,
(if the EXAMINE BEING exists, let ⊗4it⊗* do these things).
Then ask both PROVE and DISPROVE to see which is better in the particular sit,
then carry out the one with the higher recognition value. Switch if it bogs down.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Formal techniques for examining the truth of a conjecture.
INTU Inspect more closely. Look inside a box to see what it contains. Perform experiments on it.
TIES Up: Active Meta BEINGs. Down: Prove, Disprove.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2ASSUME⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {(x is true (temporarily), .90, .95, )}
FINAL {(examine consequence of case when x is true, .60, .70,)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS
DOMAIN/RANGE {not} {(a statement, a temporary world where it is true, imagination)}
ORDERING(Complete)
WORTH (.5, .5, .5, .6, .5, .5, .7, (formal: temporary, intu: irrelev), .2, (1.0 basis))
FILLIN: Never remember later; no such thing as a "model" of assuming x.
INTEREST (In the resultant world, new interesting things are discovered,.9)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Simply postulate that x is true. Tag all consequences using this that
they depend upon the assumption of x. Tag x itself as a short-lived assumption.
REPRESENTATION (ASSUMPTION, ptr to assumption, reason for assuming x) ←←perhaps
⊗5INFO GROUPING⊗*
DEFINITION Formal technique for examining hypothetical worlds, cases.
INTU Temporarily suspend disbelief. Unstated implication in all consequences.
TIES Up: Active Meta BEINGs. Side: Prove, Disprove, Test.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2DEFINE⊗* Actually, this is an elaboration of DEFINITION.FILLIN.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(ease of the concept's accessability .95, .90, learn someone's name)}
FINAL {(definite test for what is and is not in this concept, .90, .90,)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS Assign <name> the value <value>.
Temporarily, we assume that (we let) x be...
DOMAIN/RANGE {not} {(a concept, a definite handle for accessing this concept and
capable of telling whether or not a given entity is included in this concept,
complete the Definition (and Recog parts) of the BEING for this concept)}
ORDERING(Complete)
WORTH ((about .7; depends on amt and richness of Ties), .7, .6, .6, .5, .9, .7,
(formal: assumed absolute, intu: usually hi), .3, (1.0 basis))
FILLIN: Recall for later aping only; the defining itself is of no import compared to defn.
INTEREST (The intu it translates into is compatible with the existing intu for the concept)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Simply postulate that the current concept will be defined as something.
The choice of what to define it as should be in accord with any preexiting intus,
with any decent analogies to this concept, with already-observed properties/ties.
In fact, all these may suggest how to define the concept, as well as check it.
Often, one will postulate some ⊗4desired⊗* properties here; in this case it is
very important to ensure that there is at least one nonvacuous example of the β.
If it is not already named, get a name (IDEN part) for this concept.
REPRESENTATION (feature in the defn, origin, overall desirability) ←←perhaps
⊗5INFO GROUPING⊗*
DEFINITION Fill in the definition part of the current concept.
INTU Formalize precisely what we will mean when we refer to this concept.
TIES Up: Active Meta BEINGs. Side: Assume, Assign, <Complete>
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2PROVE⊗* Formally establish a statement as a valid true fact.
This actitivty might be distributed among the parts of "Proof"
⊗5RECOGNITION GROUPING⊗*
CHANGES {(x goes from conjec to theorem, .90, .80, )}
FINAL {(x is known to be true, .85, .80,),
(the truth of P is now made formally obvious and clear and believed, .90, .80,
intu: by looking closer longer, we can see more clearly and with more continuity),
(convince audience of truth of P, .85, .75, intu: lead flock down path)}
PAST {truth of x is unsure, v. imp., suspected to be true, .90, .75)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS (Result, Desired truth value for x, (false, .80, disprove),
(don't care, .80, test))}
SPECIALIZATIONS (Algorithm, specific variety,
(forward inferences, .80, natural deduction),
(backward inferences, .70, backward chaining),
(negate and try to prove F, .90, indirect proof)),
(Argument, Top-level type,
(universal statement, .80, universal proof),
(existential statement, .80, existential proof))}
DOMAIN/RANGE {not} {(a conjecture, FAIL or a proof or (at least)
a set of lemmas to prove which would establish x, an operator)}
ORDERING(Complete) The occurrence of a crucial lemma may interrupt this process.
WORTH (.8, .9, .6, .5, .8, .6, .4, (formal: 1.0, intu: medium), .3, (1.0 basis))
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Pass control to the type of proving which recognizes the curr. sit. best.
Switch if it bogs down.
If a statement L seems very clear intuitively (and empirically) and is crucial
to the prof, then call it a Lemma, defer its proof until after the conjecture
is successfully proven using L, and then prove L. ←←related to subgoal deferral.
If there is clear intu. justif. for the conjec, can it be translated into formal manips?
If some subpart's defn has v. good intu and ops, then subst its defn in for it.
Perhaps some hypothesis or conclusion can be altered (relaxed or strengthened).
Intuition: let this guide the proof if it can, but be careful.
Insane: if some generalization seems more intu. and has nicer properties, it might
be easier to prove it than the original conjecture!
One way is to prove (or access) that this is true for instances of mathematical
systems M; then access the axioms of A of M; to prove that this property
holds for some specific instance Y of some other Math System N, it suffices
to prove that each axiom in A holds (as a theorem) in Y (or, even better,
follows directly from the axioms and theorems known about any N).
Afterwards: ⊗4all⊗* theorems about M's are now known to hold for Y.
Afterwards: if failure: reexamine why we thought it was probable, modify: learn from mistakes.
If it still seems intu true, perhaps is an axiom to be assumed.
Ask user if there is some rele. but not-yet-known pf. technique.
Ibid for unknown piece of knowledge.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Formal techniques for establishing that a given conjecture is in fact true.
INTU Methods which are guaranteed to be reliable or to tell you that they have failed.
TIES Up: Test Side: Disprove, COnsider the converse←←perhaps not fed this hint
EXAMPLES {not} {bdy} (-): x turns out to be a false statement.
CONTENTS
.SKIP TO COLUMN 1
⊗2LOGICALLY DEDUCE⊗* Natural deduction.
⊗5RECOGNITION GROUPING⊗*
CHANGES {x changes its status from conjec to theorem, .80, .80, )}
FINAL {(x is known to be true, .80, .80,)}
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Algorithm, less determined, (many alternative algorithms, proof))}
SPECIALIZATIONS {(proof which progresses stepwise, in a single direction,
(forward, .60, prove directly), (backward, .60, prove indirectly))}
DOMAIN/RANGE {not} {(a conjecture, FAIL or a logically correct pf or (at least)
an ordered set of lemmas to prove which would establish x, an operator)}
ORDERING(Complete)
WORTH (.85, .8, .5, .6, .7, .6, .3, (formal: 1.0, intu: search), .2, (1.0 basis))
INTEREST (Can be used as a model for other natural deduction proofs)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here we must put in (at least pointers to) the rules of inference.
Also here will go a statement of the Law of the Excluded Middle: for any
statement S, S∨¬S. Either S is true or it is false, never neither nor both.
That is, we NEVER consider the intuitionistic approach; we always allow indirect proofs.
The alg. itself is to build up a proof (a list structure) from nothing, where
at each stage an assertion is inserted, whose justification involves only
axioms, theorems, earlier assertions in this proof, and rules of inference
applied to such entities. In addition, any assumption may be made as an
assertion, but must be so justified, and any later assertion which uses this
as part of its justif. must explicitly hold a copy of the whole assertion
in its justif. part. One rule of inf. can deal with discharging an assumption
(into an implication, or via a cases argument, etc.).
This is actually the "obvious" translation of the defn. of proof into activities.
The spirit is one of using any legal means to achieve your ends.
One will often work from both ends of P→Q, trying to find things that P
implies, and things that imply Q, until these two sets have a common member
or at least reduce the problem to a much simpler P'→Q' problem.
Hypothetical world: To establish that x→y, assume x is true temporarily, then
prove y somehow, and if sucessful untag x and assert x→y.
Alt: consider proving ¬y → ¬x instead.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Legal deductions, following the rules of logic (inference) provided.
Search a graph for a path between two given nodes.
INTU Legal moves in a game. Finding one way to get between two given board positions.
Search a graph for a path between two given nodes: dynamic programming.
TIES Up: Prove
EXAMPLES {not} {bdy} (+, bdy): ((←any axiom, $itself))
CONTENTS
.SKIP TO COLUMN 1
⊗2PROVE DIRECTLY⊗*
⊗5RECOGNITION GROUPING⊗*
CHANGES {x progresses step by step from conjec to theorem, .90, .80, ),
(problem of known-knowl. → x is made easier by expansion of rele. knwon
knowledge -- rele. new mini-theorems, .75, .95, whatever you do is true)}
FINAL {(x is known to be true, .80, .80,)}
PAST {(x is a "common" goal, compared to the few ∃ axioms and thms, .70, .60,
intu: spread outward from the uncommon, hope to hit the common soon)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Algorithm, less determined, (many alternative algorithms, proof))}
SPECIALIZATIONS {(proof which hinges on an inference equivalent to F→x, .50, vacuous truth)}
DOMAIN/RANGE {not} {(a conjecture, FAIL or a step-by-step proof or (at least)
an ordered set of lemmas to prove which would establish x, an operator)}
ORDERING(Complete)
WORTH (.85, .8, .5, .6, .7, .6, .3, (formal: 1.0, intu: search), .2, (1.0 basis))
INTEREST (Can be used as a model for other direct proofs)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS The spirit is to continually transform OK statements until the result
is produced. OK means {tautologies, axioms in this theory's foundation, previous thms,
hypotheses of this theorem-to-be}. Result means the theorem's conclusion.
Usually the form will be that of P→Q. In such cases, one builds up a chain of
implications P→A, A→B, B→....→Z, Z→Q. Intuition may set up the key intermediate
statements (say D, G) and then the problem simplifies into a collection
(in this case, one must prove P→D, D→G, and G→Q).
Cases: show that the conjecture is implied by a certain conjunction, then prove each conjunct.
Alternate view: show that the conjecture is simply a statement that a
property P holds over a set S. THen find a covering of S by {S↓i}, and
prove that P holds over each member of that covering (do this either
en masse, as a ∀ proof, or individually for all or some of the members.
ADVANTAGE: lets you apply different techniques to each bin, each S↓i.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Forward, direct deductions of new assertions; stop when desired theorem
is among those derived. A forward search by expanding a tree of assertion nodes.
INTU Forward search; whenever you reach the goal, you can stop.
In driving a car, you look to see where you are headed, to guide you.
TIES Up: Prove, Logically deduce
EXAMPLES {not} {bdy} (+, bdy): ((←any axiom, $itself))
CONTENTS
.SKIP TO COLUMN 1
⊗2CASES⊗* Wealky partition the possible situations and prove separately for each class.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(goal x replaced by conjunction of simpler goals, .90, .80, )}
FINAL {(x is known to be true, .70, .75,)}
PAST {(the intuition for the examples of x is not uniform, .90, .80,
intu: x is true for diff. reasons in diff. situations, so diff. pfs. ∃)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS {(x is already a conjunction, prove each conjunct, .60, idea of ∧),
(x gets split into proofs of (a → x) and (¬a → x), .60, ) }
DOMAIN/RANGE {not} {(a conjecture and a partitioning of all possible situations,
FAIL or a step-by-step proof or (at least)
an ordered set of lemmas to prove which would establish x, an operator),
(conjec, partitioning and a proof for each class, very costly search if unintuitive)}
ORDERING(Complete)
WORTH (.7, .8, .4, .5, .6, .8, .4, (formal: 1.0, intu: search), .4, (1.0 basis))
INTEREST (The proof for each case is easy and very different and diff. intuition)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS The basic algorithm is: (i) identify the partition (a taut. disjunction),
(alternate view: break x up into a conjunction of simpler clauses which imply x.
(ii) for each class, try to prove it, try to establish each conjunct independently,
especially: use intuition.
Alternate view: show that the conjecture is simply a statement that a
property P holds over a set S. Then find a covering of S by {S↓i}, and
prove that P holds over each member of that covering (do this either
en masse, as a ∀ proof, or individually for all or some of the members.
ADVANTAGE: lets you apply different techniques to each bin, each S↓i.
Heurisitcs for the division process: Say x is the statement ∀z, P(z).
If there are just a few types of z's, use that division tentatively.
After distinguishing some types of z's, group the rest as one final class.
Sometimes: group the disting. z's together as just one case.
Ways that a type of z can be disting: bdy, degenerate, current variable value
If feature f is known to be relevant, try to subdivide the z's along f.
To prove a disjunction, prove one disjunct while assuming the negation of each
of the rest.
To prove a conjunction, prove the easiest of the conjuncts, say A; then prove
the easiest remaining conjunct, say B, noticing that A is a true (and probably
relevant) mini-theorem which can be used; then prove the easiest remaining conjunct
(probably using the facts that A and B are known to be true), etc.
Hint for the above: do each of the above demonstrations, but in the opposite order.
That is, choose the hardest conjunct, say Z. First try to prove it, while
assuming that all the other conjuncts are true. If this succeeds, recurse in
this direction (find the next hardest, say Y, and prove assuming that all the
others except for Z are already known to be mini-theorems). The point of this is
that the proofs of A, B,... may be easy anyway, but the proof of A∧...∧Y→Z
will probably still be hard; if you are going to fail, it is important to find
out as quickly as possible, to try a new tack. One slight fixup here is to
reassess the difficulty of the conjuncts, and reorder them.
To prove that several statements are all equivalent, the obvious Cases argument
would be to divide up the proof into a separate one for each A↓i↔A↓j, perhaps
each would recurse here again into separate implication proofs each way.
A faster, and logically valid, method is to order the statements, then
prove the ring of single implication A↓1→A↓2→...→A↓[n-1]→A↓n→A↓1.
The intuition here is that of a circularly linked list: to proceed from
any point of the loop to any other, just keep moving around it and you'll ge there.
REPRESENTATION (distinguishing character of this case, statement, proof)*
⊗5INFO GROUPING⊗*
DEFINITION Forward, slightly indirect subdivision of the problem into simulataneous
subgoals. Divide the possible worlds along some partition, then enter each one
in turn and establish the conjecture.
To formally include this type of proof into natural deduction, introduce the
disjunction D of all the possible cases, prove that D is universally true (usually trivial),
then present the proof that each disjunct of D implies x, and then discharge
the disjuncts of D in turn by replacing them by x, and finally replace x∨x∨x∨... by x.
No effort s made to ensure a strong partition (absolutely disjoint classes);
the only requirement is that the partition be complete (cover the entire set
of possible alternatives). The disjointness (which often will speed the proofs
up a bit) can be introduced later, after the concepts of set-disjointness and
equivalence-relations have been discovered and made into β's and developed.
INTU The more specific the world, the easier it is to prove a true conjecture.
The extreme case of this is the absolutely specific world of an example.
TIES Up: Prove, Logically deduce
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2BACKWARD CHAINING⊗* Produce a direct proof, but by working backward from the goal.
⊗5RECOGNITION GROUPING⊗*
CHANGES {x goes step by step from conjec to theorem, .90, .80, ),
(problem of known-knowl. → x is made easier by simplification of x, goes to
the problem of known-knowl → simpler-x, .75, .95, whatever you do is true)}
FINAL {(x is known to be true, .80, .80,)}
PAST {(x is a "rare" goal, compared to the many ∃ axioms and thms, .70, .60,
intu: spread outward from the uncommon, hope to hit the common soon)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Algorithm, less determined, (many alternative algorithms, proof))}
SPECIALIZATIONS
DOMAIN/RANGE {not} {(a conjecture, FAIL or a step-by-step proof or (at least)
an ordered set of lemmas to prove which would establish x, an operator)}
ORDERING(Complete)
WORTH (.80, .8, .5, .5, .75, .55, .35, (formal: 1.0, intu: search), .2, (1.0 basis))
INTEREST (Can be used as a model for other backward chaining proofs)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here we must put in (at least pointers to) the rules of inference, but
written in a backward applicable way. For example, modus ponens says that
from A, to infer B, you must prove A→B. In a backward form, it says that to
infer B, pick any A, then try to prove both A and A→B (often, A is constrined
to be known to be true, so its proof is unnecessary). Viewed in this way,
a proof is built up, starting with the goal; each new entry should justify
the one which was just inserted before this point in time. Finally, an
entry will be made which needs no justification at all, and we can stop.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Backward, direct deductions of new equivalent formulations of the goal,
each one hopefully simpler than the previous ones. Stop when an OK statement
(thm, axiom, True, hypothesis of this thm) is found.
INTU Backward search, from the goal. Stop when you have built up a complete proof.
TIES Up: Prove, logically deduce
EXAMPLES {not} {bdy} (+, bdy): ((←any axiom, $itself))
CONTENTS
.SKIP TO COLUMN 1
⊗2PROVE INDIRECTLY⊗* Assume the conjec. is false, and derive a contradiction.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(x is known to be true, .80, .80,)}
PAST {(x is so "true" that its negation should easily be shown to be absurd,
.90, .85, intu: assume (x or not x), show not(not x)) is the case),
(proving something about an infinite set, .50, .60, can't get there one step at a time),
(proving that a set is infinite, .85, .80, good because the negation is manageable),
(hard to do a direct proof in either direction, .60, .90, intu: one of the alts. must work)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Algorithm, less determined, (many alternative algorithms, proof))}
SPECIALIZATIONS
DOMAIN/RANGE {not} {(a conjecture, FAIL or a step-by-step proof or (very rarely)
an ordered set of lemmas to prove which would show not-x is absurd, an op)}
ORDERING(Complete)
WORTH (.4, .9, .6, .5, .8, .6, .45, (formal: 1.0, intu: double negative), .25, (1.0 basis))
INTEREST (Can be used as a model for other indirect proofs)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here we must put in (at least pointers to) the techniques of deriving a
contradiction (and, even more basic: the techniques of negating, qv).
The first step is to ASSUME (NEGATION ( conjecture)).
From this we do a direct proof (almost always forward) to a contradiction
(either F, or A ∧ not A, or $original-conjecture). From not-A → F we
conclude (via modus tollins) that T → A, i.e., that A is a theorem.
A common mode of the direct disproof is by pigeonholing.
To establish A→B: assume A, assume ¬B, then derive a contradiction.
Often, this is of the form: ¬A, B, False, or C∧¬C for some C.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Rephrase the task to one of showing that a certain statement is absurd,
that from it we can derive its own negation (and/or F and/or any other falsehood.
INTU In politics: Win by attacking your opponent rather than supporting yourself.
TIES Up: Prove
EXAMPLES {not} {bdy} (+, bdy): x is any axiom. ((x,x)(not-x,goal))
CONTENTS
.SKIP TO COLUMN 1
⊗2PROVE ∀'s⊗* Establishing universal conjectures, statements of generality.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(S is known to be true, .80, .80,)}
PAST {(S is of the form ∀x in set X, P(x) holds, .90, .80,intu: direct),
(ibid, plus X has some int. properties besides its defn, .85, .90, intu: reserve power)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Domain, less determined, (many alternative formats of S, proof))}
Fillin: may be easier to prove P holds on a superset of X which has nicer props.
SPECIALIZATIONS
DOMAIN/RANGE {not} {(a conjecture S of the form ∀x in X, P(x);
FAIL or a step-by-step proof or an indirect proof or an ordered set of
lemmas to prove which would establish S, an operator)}
ORDERING(Complete)
WORTH (.9, .9, .6, .5, .7, .65, .4, (formal: 1.0, intu: a new property of X), .3, (1.0 basis))
INTEREST (Can be used as a model for other universal assertion proofs)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here we must put in the techniques and hints for establishing a universal
property over an entire set. The insane heuristic: it may be easier to establish
a more rigorous property than P, it may be easier to eastablish it over a
superset of X. Cases: one might wish to partition X and prove separately for
each member of the partition (often only a covering). Indirect: make sure that
this wasn't originally an ∃; negate it into ∃ form and try to prove it is
inconsistent with the world. Representative: pick a prototypical member x
from X, never say which one it is, then show it has property P.
Mathematical Induction: q.v.; let Y be the subset of X over which P holds;
prove that X is contained in Y, that Y is all of X; often by building up Y
one element at a time, then showing that eventually any prototypical element
x of X will find its way into Y. Trick of exclusion: to show that ∀x≠bεX.P(x) holds,
it suffices to show that X = {b}∪{zεX | P(z)}.
An alternative: show that P' holds on all of X, where P'(x) = P(x) ∨ x=b.
An alternative: prove that P holds on X' = {xεX | x≠b} = X-{b}; that is, the
proof proceeds by assuming that one additional property of the set is y¬ε of it.
Directly prove ∀xεX.P(x).
Let x be an element of X. While x shall remain fixed throughout this proof,
we never use any property of x except those known to hold for every element
of X. Try to prove that P holds on element x.
Modification: consider cases: cover X with subsets {X↓i}, then prove for each X↓i.
Indirectly prove ∀xεX.P(x).
Assume the negation of the conjecture, namely ∃xεX. ¬P(x). So the existence
of such an element in X is guaranteed. Let z be such an element. That is,
we assume that z is a member of X, and that P does not hold for z. Now we
must derive a contradiction (often: P(z), z¬εX, C∧¬C, X=PHI, etc.)
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Demonstration that property P is implied by the property defining set X.
Prove that all members of set X satisfy P.
INTU It turns out that not only do all x in X satisfy the defining criteria for X,
they also satisfy P. The defining predicate must therefore imply P non-obviously.
TIES Up: Prove
EXAMPLES {not} {bdy} (+, bdy): S is the assertion ∀x in X, P(x), with P one of these:
(x is in X), T, x=x.
(-, bdy): P is one of these: (x is not in X), F, x≠x.
CONTENTS
.SKIP TO COLUMN 1
⊗2MATHEMATICALLY INDUCE⊗*
⊗5RECOGNITION GROUPING⊗* This is very important part, actually!
CHANGES
FINAL {(statement true for ⊗4all⊗* members of an ordered structure, .90, .80,),
(P(x) true for ⊗4all⊗* values of x in an ordered struc., .90, .80,)}
PAST {(conjec. to be proved deals with all elements of an infinite set, .70, .60)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Prove, demonstrate.
SPECIALIZATIONS
DOMAIN/RANGE {not} {(a conjecture about all elements of a totally ordered structure,
FAIL or a theorem (perhaps depending on a set of lemmas), an operator)}
In general, the conjecture will be of the form ∀xεinf.set,P(x).
ORDERING(Complete)
WORTH (.8, .7, .6, .4, .7, .5, .4, (formal: 1.0, intu: decent), .2, (1.0 basis))
FILLIN: During the induction, a new β will probably be created. To avoid
clutter, once it is begun the effort to complete the induction will
be sustained at a nearly uninterruptable level. When it finally
succeeds or fails, the result may be saved as a new β, but the
process of induction β will die (except: possible retention for
use as a model for future inductions; iff very distinctive)
INTEREST
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Below are both an abstract and a concrete procedural rendering of the defn:
Abstract: To show that property Q holds on structure I, consider the set
SQ = {xεI | Q(x)}. It suffices to show that SQ=I.
If we already know (thm or axiom) that "any subset of I which satisfies P
must be all of I (equal to I itself)", then it suffices to show P(SQ).
Concrete: There are three important activities here, usually done in order:
Hypothesize: form the inductive hypothesis, typically of the form
P holds for some member x (or: for x and all earlier membs) of this ord. struc.
This will eventually let you conclude that P holds over the whole struc.
FILLIN: don't be afraid to strengthen this if the stronger form is still
intuitive, and empir. on first few eles., and makes Recurse easier.
Weaken the hyp. if it seems false, or unprovable otherwise.
esp: the weakened form can be used as a lemma for ⊗4this⊗* pf.
Base: prove that P holds for the first element of the ordered structure S.
FILLIN: If we must prove P(x) for x in S, the base step is usually
to prove P is true on the first element(s) of S, simplest cases of S.
Later, during Recurse, if some additional condition would help
and is true of these cases, then add it to the hypothesis P.
ALGORITHM: Often, this case is vacouously true, or a known earlier fact.
It is usually specific enough to examine as a concrete entity/example.
If it still is hard, but intu. clear, consider making it a lemma.
Recurse: assuming that P holds for all elements of S before e, prove P(e).
Alt: assume that P holds for e and for each pred↑*(e). Show that P holds
on each successor of e. Often, there will only exist one successor.
If you prove Base for first k elements, then in proving Recurse you can
assume that e has at least k predessors.
Conversion: once the induction is completed, how to transform the proof
in general into a proof for a specific case of the hypothesis.
REPRESENTATION (S, P phrased as a predicate on elements of S,(base)*, recurse)
VIEWS Perhaps fed in later by the user, perhaps discovered: well-ordering axiom, Ax. of choice;
notice that ttese are not meaningful until concept of singleton (hence Function) evolves.
⊗5INFO GROUPING⊗*
DEFINITION Formal technique which lets you prove that every member of an ordered
structure (list or oset, typically infinite) satisfies a certain predicate.
INTU Show that you start, then prove you always go on; conclude you never stop.
TIES Up: Active Meta BEINGs, Prove. Tied to RECURSION, if that is provided.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2PROVE EXISTENCE⊗* Establishing existential conjectures, statements of existence.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(S is known to be true, .80, .80,),
(at least one particular x↓o in X is known to satisfy a given property,
.90, .75, intu: somehow show that there is somebody like that)}
PAST {(S is of the form ∃x in set X, P(x) holds, .90, .80, intu: direct),
(ibid, plus X has some int. properties besides its defn, .50, .85, intu: reserve power)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Domain, less determined, (many alternative formats of S, proof))}
Fillin: may be easier to prove P holds somewhere on a subset of X which has nicer props.
May be easier to show ∀x in W, P(x), where W≠PHI is ⊂ X.
SPECIALIZATIONS {(Task, satisfaction set of P over X, (singleton, .90, ∃1 ←←discovered),
(non-null, .70, ∃ -- this BEING itself),
(null, .70, there does not exist; equivalent to ∀x in X, NOT(P(x))))}
DOMAIN/RANGE {not} {(a conjecture S of the form ∃x in X, P(x);
FAIL or an actual example or an indirect proof or an ordered set of
lemmas to prove which would establish S, an operator)}
ORDERING(Complete)
WORTH (.8, .8, .5, .5, .6, .6, .5, (formal: 1.0, intu: ensure it exists), .25, (1.0 basis))
INTEREST (Can be used as a model for other existential assertion proofs)
(Some use is known for the particular element satisfying P, once it is found,.7)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here we must put in the techniques and hints for establishing an existence.
Constructive: find such an x.
The insane heuristic: it may be easier to establish the existence of an x which
satisfies a stronger property than P,
it may be easier to eastablish ∃ in a particular small subset of X.
Cases: one might wish to partition X and prove the dijunction of the existence
in each member of the partition (often only a covering).
Indirect: make sure that this wasn't originally an ∀;
negate it into ∀ form and try to prove it is inconsistent with the world.
Recast: Consider PP = the set defined by property P. Must show that PP∩X ≠ PHI.
Recast: Consider PX = the property defining X. Must show that
∃p in PP which satisfies PX(p). Ensure that this was not done before!
Analogue to ∀-Induction: let Y be the subset of X over which P holds;
prove that Y is not empty. Insane: prove that Y contains some given subset of
Z of X which is trivially non-empty.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Demonstration that property P is intersects the property defining set X.
Prove that some member of set X satisfies P.
INTU It turns out that not only do all x in X satisfy the defining criteria for X,
some of them also satisfy P.
The defining predicate must therefore not preclude P.
PP and X intersect.
TIES Up: Prove
EXAMPLES {not} {bdy} (+, bdy): S is the assertion ∃x in X, P(x), with P one of these:
(x is in X), T, x=x, x=x↓o with x↓o known to be in X.
(-, bdy): P is one of these: (x is not in X), F, x≠x, x=x↓o (known not to be in X)
CONTENTS
.SKIP TO COLUMN 1
⊗2CONSTRUCTIVELY PROVE EXISTENCE⊗* Build up an example to prove one exists.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(S is known to be true, .75, .70,),
(at least one particular x↓o in X is known to satisfy a given property,
.80, .75, intu: to show that there is somebody like that, find such a critter)}
PAST {(S is of the form ∃x in set X, P(x) holds, .80, .70, intu: direct),
(ibid, plus X is accessable and not too big, .90, .95, intu: exhaustive search),
(ibid, plus X has some int. properties besides its defn, .50, .85, intu: reserve power)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Algorithm, less determined, (many alternatives,.70, prove ∃ any way))}
SPECIALIZATIONS {(Task, satisfaction set of P over X, (singleton, .90, constructively find unique x),
(non-null, .70, constructively show ∃ -- this BEING itself),
(null, .70, there does not exist; equivalent to direct pf of ∀x in X, NOT(P(x)))}
DOMAIN/RANGE {not} {(a conjecture S of the form ∃x in X, P(x);
FAIL or an actual example -- a specific element of X satisfying P, an operator)}
ORDERING(Complete)
WORTH (.8, .7, .6, .6, .5, .6, .5, (formal: 1.0, intu: find one which ∃), .25, (1.0 basis))
INTEREST (Can be used as a model for other constructive existential assertion proofs)
(Some use is known for the particular element satisfying P, once it is found,.7)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here we must put in the techniques and hints for actually finding a specific
element x of a given set X which satisfies a particular property P.
Nest: Show that x must be in some proper subset X' of X, then that it must
be in X'' (a small subset of X'), etc., until some X↑(↑n↑) is a singleton.
The insane heuristic: it may be easier to find the set of all x in X satisfying P.
It may be easier to find an x satisfying a stronger property than P.
It may be easier to prove that ∀x in X'⊂X, P(x), also that X'≠PHI.
It may be easier to eastablish ∃ in a particular small subset of X.
Cases: one might wish to partition X and simult. search each member.
Indirect: find all the elements in X which don't satisfy P(x) and cross them out.
Recast: Consider PP = the set defined by property P. Must find x in PP∩X.
Recast: Consider PX = the property defining X. Must find an element p in PP
which satisfies PX(p). Ensure that this was not recast before!
Direct: Take known specific entities and ops (often their inverses, too), and
build up a new entity x (which is intuitively believed to show existence).
Then you mus show that x is in fact in X, and that P does hold on x.
Exhaustion: If X is little and P (or its negation) is easy/quick to test,
then search all of X, seiving with P as the test criterion.
Dual: Consider PP = {x | P(x)} and PX (the property εX). Recast the problem as
∃xεPP. PX(x). Don't do this more than once for the same problem, though!
Coincidence: We know, via an OK statement (earlier thm, axiom, hypothesis
about the set X), that ∃zεZ.P(z). Consider such a z. It may be the desired
member of X; if not, set up an analogy Z↔X and try to map z over.
Slightly more general: z satisfies P' which is close to P in some sense.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Find some element satisfying both property P and the property defining set X.
Exhibit some member of set X satisfying P.
INTU Seive through X with a P-seive, catching some x.
Recast: construct PP and use PX-seive.
Find an element in the intersection of PP and X.
TIES Up: Prove, ∃
EXAMPLES {not} {bdy} (bdy): S is the assertion ∃x in {y}/PHI, P(x).
This is + if P(y), - if not(P(y)).
CONTENTS
.SKIP TO COLUMN 1
⊗2NONCONSTRUCTIVELY DEDUCE EXISTENCE⊗* Prove that some such entity, though unknown, ⊗4must⊗* exist.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL {(S is known to be true, .75, .70,)}
PAST {(S is of the form ∃x in set X, P(x) holds, .80, .70, intu: direct),
(ibid, plus X is inaccessable and/or huge, .90, .95, intu: can't do exhaus. search),
(ibid, plus X has some int. properties besides its defn, .50, .85, intu: reserve power)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS {(Algorithm, less determined, (many alternatives,.70, prove ∃ any way))}
SPECIALIZATIONS
DOMAIN/RANGE {not} {(a conjecture S of the form ∃x in X, P(x);
FAIL or an indirect proof that such an x must exist in X, an operator)}
ORDERING(Complete)
WORTH (.7, .7, .5, .6, .7, .5, .4, (formal: 1.0, intu: can't construct one), .2, (1.0 basis))
INTEREST (Can be used as a model for other nonconstructive existential assertion proofs)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Here we must put in the techniques and hints for proving ∃ without actually
finding a satisfactory element x. We are assuming that the conjec. is ∃xεX.P(x).
Indirect: Let N={yεX | ¬P(y)}. Prove that N is not all of X.
Often: do this by showing that N possesses some property that X doesn't.
Sometimes: show X satisfies some property that N doesn't.
Indirect: Assume that N=X and get a contradiction.
Nest: Show that x must exist in some superset X' of X, then that it must
be in X'' (a subset of X'), etc., until some X↑(↑n↑) is ⊂ X.
The insane heuristic:
it may be easier to prove the set of all x in X satisfying P ≠ PHI.
It may be easier to prove ∃x satisfying a stronger property than P.
It may be easier to prove that ∃X'⊂X,X'≠PHI, s.t. ∀x in X', P(x).
It may be easier to establish ∃ in some nonnullsubset of X.
Cases: one might wish to partition X and indirectly prove disjunction.
Recast: Consider PP = the set defined by property P. Prove ∃x in PP∩X.
Recast: Consider PX = the property defining X. Nonconstruc. prove ∃p in PP
which satisfies PX(p). Ensure that this was not recast before!
Usually: Negate and show that the resultant ∀ conjecture is absurd.
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Without actually finding one, prove that some element of X satisfies P.
Show that the assertion that PX and P (or that X and PP) are disjoint is absurd.
INTU Show that there must be some such satisfactory element, even if we can't name it.
It is unthinkable that no element of X would satisfy P.
TIES Up: Prove, ∃
EXAMPLES {not} {bdy} (bdy): S is the assertion ∃x in Universe, P(x), where
P is known to be satsifiable (+) or unsatisfiable (-).
CONTENTS
.SKIP TO COLUMN 1
⊗2DISPROVE⊗* Establish definitively that conjecture x is false, invalid.
⊗5RECOGNITION GROUPING⊗*
CHANGES {x goes from conjec to falsehood, .90, .80, )}
FINAL {(x is known to be false, .85, .80,)}
PAST {truth of x is unsure, v. imp., suspected to be false, .90, .75)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS (Result, Desired truth value for x, (true, .80, prove),
(don't care, .80, test))}
SPECIALIZATIONS (Algorithm, specific variety,
(forward inferences and specializations of x leading to F, .80, counterexample),
(try to prove negation(x), .80, indirect disproof))}
DOMAIN/RANGE {not} {(a conjecture, FAIL or a disproof or a counterexample, op)}
ORDERING(Complete)
WORTH (.7, .8, .6, .5, .8, .6, .4, (formal: 1.0, intu: medium), .4, (1.0 basis))
INTEREST (The conjecture was believed to be true until this was discovered)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Pass control to the type of disproving which recognizes the curr. sit. best.
Switch if it bogs down.
Pigeonholing: show that the conjecture is just a claim of the form "each x belongs to some
class in this partitioning", then find an x which you can show belongs to none,
or show that each pigeonhole only holds one x but there are more x's than holes,
and no single x can fit in more than or less than one hole.
Cases: show that the conjecture implies a disjunction, then disprove each disjunct.
Strengthen: show that the conjecture implies a conjunction, then disprove one conjunct.
Recast: prove that the negation of the statement is a theorem (don't recast twice!)
Instance: the conjecture is a statment of generality: find one exception.
Instance: statement is ∃xεX.P(x). Prove ∀xεX. ¬P(x).
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Formal techniques for establishing that a given conjecture is in fact F.
INTU Methods which are guaranteed to be reliable or to tell you that they have failed.
TIES Up: Test Side: Prove.
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2CONSTRUCTIVELY DISPROVE⊗* Directly establish the falsity.
Some of this activity might be distributed among the parts of "Counterexample"
For the moment, we shall put all our techniques in one category; if this really
warrants a new β during our hand simulation, we shall fill it in before coding.
⊗2INDIRECTLY DISPROVE⊗* Generally nonconstructive.
For the moment, we shall put all our techniques in one category; if this really
warrants a new β during our hand simulation, we shall fill it in before coding.
⊗2DEBUG⊗* Correct, eliminate a bug.
⊗5RECOGNITION GROUPING⊗*
CHANGES {(perfection of piece of knowledge/code, .80, .85, repair)}
FINAL
PAST {(error message from system: interrupts go here, .90, .95, alterations of clothes)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS Undo, reverse, eliminate, reconcile, solve, fix.
SPECIALIZATIONS Define.
DOMAIN/RANGE (situations in which bugs occur, those in which they have gone away,repair operation),
(sits in which imp. x malfunctions, sit in which x is no longer considered important, give up)
ORDERING
WORTH (.1, .4, .4, .5, .6, .5, .4, (formal: empirical; intu: fallability), .1, (1.0 basis))
FILLIN: Generally, one will work until the bug goes away, then let the new debug β die.
Retain, however, some indication of how it was fixed and why that way.
INTEREST The origin was unexpected, it requires a modification of some previous beliefs.
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Look up in table the meaning of the error message, access canned routine to fix.
Scrutinize the origin to see why this is syntactically (or sem) illegal in LISP.
Decide whether the effort to fix it is becoming too costly, then postpone the goal.
REPRESENTATION (bug, (effort, result)*)
VIEWS (communicate a better or more detailed version of trigger to op-system)
(understand the contradiction well enough to correct it and prevent future occurrences)
⊗5INFO GROUPING⊗*
DEFINITION A bug has been found and is impeding progress, or is degrading the reliability of
the system's beliefs. It is necessary to understand this to be able to correct
the situation. Often, the way to fix it is clear simply from the error message
received; occasionally some infeence will be required to see how to fix it up.
No "syntactic" definition should be alone here; a "semantic" one is a
practical necessity.
INTU Unbearable situation is being dealt with. Handle an interrupt. Close credability gap.
Alter clothes which don't fit. Fix a malfunctioning car. Wise up.
TIES Up: Active Meta BEING
EXAMPLES {not} {bdy}
CONTENTS
.SKIP TO COLUMN 1
⊗2COMMUNICATE⊗* Create, translate, and analyze messages.
⊗5RECOGNITION GROUPING⊗*
CHANGES {intelligibility of message M, .80, .85, )}
FINAL {(message M can be understood, .80, .80,)}
PAST {(X wants Y informed of M but Y can't understand M directly, .90, .90)}
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS (contents, complexity, (simple enough,.9, no transformation needed)
DOMAIN/RANGE {not} {(message in one format, message in another format, an operator)}
ORDERING(Complete)
WORTH (.3, .2, .02, .4, .7, .5, .4, (formal: low, intu: hifh), .5, (1.0 basis))
FILLIN: almost always destroy after message is transformed successfully or otherwise.
INTEREST There is a huge family difference between receiver and sender.
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS Two main paths: communicate with user or with other BEINGs.
Along the former are special routines for each direction of information flow.
The latter has ways for creating messages rich enough with imagery, intu, examples
to be understood by any other BEING, other techniques, etc.
REPRESENTATION (part of original message, (change, result, why)* )*
⊗5INFO GROUPING⊗*
DEFINITION Informal techniques for manipulating information which is to be passed.
INTU Alterations on a dress passed down to another. Translate a book into another lang.
TIES Up: Active Meta BEINGs. Down: Communicate with user, InterBEING Communicate.
EXAMPLES {not} {bdy} (bdy,+): message is on boundary, e.g. just a BEING part.
(-): no translation whatsoever is necessary
CONTENTS
.SKIP TO COLUMN 1
⊗2COMMUNIC. with USER⊗*
For now we assume perfect translation capabilities. The simulation and the actual
running first phase will help constrain what must be present here.
⊗2TRANSLATE English into Beings⊗*
⊗2TRANSLATE Beings into English⊗*
⊗2USER⊗* Model of the human user.
⊗2COMMUNIC. with other BEINGs⊗*
For the moment, we shall put all our techniques in one category; if this really
warrants a new β during our hand simulation, we shall fill it in before coding.
⊗2RELATION META BEINGs⊗* Active meta-Beings which are relations more than operations.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗* It is not clear whether any ⊗4new⊗* β's in this category will ever be created.
GENERALIZATIONS
SPECIALIZATIONS {(justif, degree of formality maintained,
(absolute, .40, not any known initially),
(hazy, .70, all currnelt known)),
(domain/range, restricted to known type of meta-Being,
(both math systems, .70, isomorphism),
(both systems of axioms, .60, categoricity))}
DOMAIN/RANGE {not} {(some meta-β's (esp. static meta β's),{T,F}, relation/pred)}
ORDERING(Complete)
WORTH (.4, .4, .4, .5, .8, .3, .4, (formal: low, intu: variable), .4, (1.0 basis))
INTEREST (Quite surprising that there is any close tie between the args)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Activities which result in the tying of existing (usually static) meta β material.
That is, a relation on a cross-product of static meta-BEINGs.
Alt: an Active Meta Being which has the character of a relation more than an operation.
INTU Some similarity between two very high level constructs. A very abstract relationship.
TIES Up: Active meta BEING, Relation.
EXAMPLES {not} {bdy}
CONTENTS Not clear that these β's will ever have Contents in any meaningful sense.
.SKIP TO COLUMN 1
⊗2ISOMORPHISM⊗* Equivalence of a pair of mathematical theories .
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS Equivalence
DOMAIN/RANGE {not} {(AMathTheory↑2, {T,F}, relation/pred)}
ORDERING(Complete)
WORTH (.5, .5, .4, .5, .8, .3, .4, (formal: low, intu: variable), .5, (1.0 basis))
INTEREST (The two systems arose from different motivations, have different instances)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Only a fuzzy definition exists. See examples and intu parts for more info.
Let M be a mathematical theory with basis B, axioms A, and let M' be a mathematical
system with basis B' and axioms A'. We then say that M and M' are isomorphic
if there exists a complete analogy R between B and B', in the sense that each
structure S has a correspondent S', similarly each active, each distinguished
element, each distinguished subset, and they all satisfy (f(x))' = f'(x').
In addition, the analogy must be an operation which is as specific as possible
while being complete: it should be single-valued, defined on all of B, the
image of B should be all of B', distinguished elements should map into '-distinguished
elements, etc.
We use the sets of axioms, A and A', to help prove the needed facts about the
equality between a certain f working on a certain S, and the f' operation at work
on the S' structure. That is, we use the axioms to prove all the needed facts
of the form (f(x))' = f'(x') which are demanded by the definition above.
INTU Resemblance, similarity, family traits. Equivalence for all mathematical purposes.
TIES Up: Relation meta BEING, Relation.
EXAMPLES {not} {bdy} see pages 225,226,228,229 of Kershner.
CONTENTS
.SKIP TO COLUMN 1
⊗2CATEGORICITY⊗* Uniqueness of any set of axioms for a math theory with a given basis.
⊗5RECOGNITION GROUPING⊗*
CHANGES
FINAL
PAST
IDEN {not}{quick}
⊗5ALTER GROUPING⊗*
GENERALIZATIONS
SPECIALIZATIONS Uniqueness (if this exists in the system)
DOMAIN/RANGE {not} {(AAxiom-set↑2, {T,F}, relation/pred)}
ORDERING(Complete)
WORTH (.3, .4, .6, .4, .8, .2, .3, (formal: fuzzy, intu: variable), .3, (1.0 basis))
This is often undesirable, since it means that there can't be more than one
meaningfully different instance of any mathematical system with these axioms
as the axioms of its foundation; this saves time from being wasted looking for more.
INTEREST (There are two different instances (with this set of axioms) that appear distinct)
OPERATIONS
⊗5ACT GROUPING⊗*
ALGORITHMS
REPRESENTATION
⊗5INFO GROUPING⊗*
DEFINITION Only a fuzzy definition exists. See examples and intu parts for more info.
We say that a mathematical system is of type A iff its set of foundation axioms is A.
We say that A is categorical iff any two mathematical theories of type A are
necessarily isomorphic.
The fuzziness arises from the dependence upon the fuzzy notion of isomorphism.
INTU Abstractly unique. The rules of the game are so constraining that there can be
only one legal sequence of moves, only one playable game.
TIES Up: Relation meta BEING, Relation.
Analogy: categoricity is to consistency as uniqueness is to existence.
EXAMPLES {not} {bdy} it shouldn't actually be told these things: (+): Natural numbers
(-): Groups
CONTENTS
.SKIP TO COLUMN 1
⊗3ENVIRONMENT⊗* Model of system functions.
What the BEINGs must know about the env. should be made clear during the simulation.
⊗2BELIEF⊗*
⊗2INTERESTINGNESS⊗* ⊗7Notice this differs from the archetypical part-name Interest.⊗*
⊗2CONTROL⊗*
.PORTION CONTENTS
.NOFILL
.PREFACE 10 MILLS
.EVERY FOOTING(,,)
.ONCE CENTER
@2↓_TABLE OF CONTENTS_↓⊗*
.TURN ON "{∞→"
.NARROW 20, 20
.SKIP 3
.RECEIVE